tnt 1.0.2

Simple runtime validated proofs in number theory
1
2
3
4
5
6
<var> ::= { <lowercase_letter> | <var> "'" }
<arith_op> ::= { "+" | "*" }
<expr> ::= { "0" | var | "(" <expr> <arith_op> <expr> ")" | "S" <expr> }
<quant> ::= { "A" <var> ":" | "E" <var> ":" | "~" <quant> }
<logical_op> ::= { "&" | "|" | ">" }
<formula> ::= {  <expr> "=" <expr> | "[" <formula> <logical_op> <formula> "]" | <quant> <formula> }