lean2/tests/lean/single.lean
Leonardo de Moura 08718e33dc refactor(builtin): only load the kernel and natural numbers by default
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 13:35:37 -08:00

7 lines
130 B
Text

Import int.
Variables a b c : Int.
Show a + b + c.
Check a + b.
Exit.
(* the following line should be executed *)
Check a + true.