lean2/tests/lean/module.lean
2013-12-26 13:21:36 -08:00

2 lines
No EOL
91 B
Text

(* The following command should fail because the IdMacro is not defined *)
Show IdMacro 20.