Choose syntax for corpus

fritzo / pomagma

An inference engine for extensional untyped λ-calculus

Other

17 stars 2 forks source link

Choose syntax for corpus #33

Closed fritzo closed 9 years ago

fritzo commented 9 years ago

The corpus will soon be revived, and it needs a format. Markdown with some simple code format seems best. This issue requires:

settling on a code syntax
sketching literate programming transforms in the compiler

fritzo commented 9 years ago

Jupyter notebooks appear to be a better choice than markdown.

fritzo commented 9 years ago

Syntax should be list of facts, i.e. theories:

# This is already a format pomagma understands.
EQUAL compose FUN f FUN g FUN x APP f APP g x  # definition-as-equation
EQUAL B compose                                # assertion-as-equation
LESS BOT compose                               # additional assertions
LESS compose TOP

If we want to get fancier in the future, then put the lines in cells of google sheets, or make a fancy structured-editor front-end. But this is a good intermediate format that is already human-editable.