michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/tests/lean/interactive
History
Leonardo de Moura 7772c16033 refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque 
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking  a valid term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 12:47:47 -08:00
..
config.lean feat(frontends/lean): rename command Set to SetOption 2013-12-18 21:18:48 -08:00
config.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
elab6.lean refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque 2013-12-20 12:47:47 -08:00
elab6.lean.expected.out feat(library/elaborator): only expand definitions that are not marked as hidden 2013-12-20 02:16:49 -08:00
t1.lean feat(library/tactic): use _tac suffix instead of _tactic like Isabelle 2013-12-05 20:06:32 -08:00
t1.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
t2.lean feat(library/tactic): use _tac suffix instead of _tactic like Isabelle 2013-12-05 20:06:32 -08:00
t2.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
t3.lean feat(library/tactic): use _tac suffix instead of _tactic like Isabelle 2013-12-05 20:06:32 -08:00
t3.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
t4.lean fix(frontends/lean/parser): remove unnecessary '#' after error 2013-12-05 17:27:08 -08:00
t4.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
t5.lean feat(library/tactic): use _tac suffix instead of _tactic like Isabelle 2013-12-05 20:06:32 -08:00
t5.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
t6.lean feat(library/tactic): use _tac suffix instead of _tactic like Isabelle 2013-12-05 20:06:32 -08:00
t6.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
t7.lean feat(frontends/lean/parser): add assumption command, and allow Lean expressions (proof terms) to be used with apply tactic command 2013-12-05 20:08:51 -08:00
t7.lean.expected.out fix(frontends/lean/pp): make sure pp and parser are using the same precedences 2013-12-19 12:46:14 -08:00
t8.lean feat(frontends/lean): rename command Set to SetOption 2013-12-18 21:18:48 -08:00
t8.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
t9.lean fix(frontends/lean/parser): display failed state in noninteractive mode, stop processing tactic commands when a Lean command is found 2013-12-06 05:13:29 -08:00
t9.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
t10.lean fix(frontends/lean/parser): display failed state in noninteractive mode, stop processing tactic commands when a Lean command is found 2013-12-06 05:13:29 -08:00
t10.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
t11.lean fix(frontends/lean/notation): change the precedence of '->' 2013-12-06 13:23:24 -08:00
t11.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
t12.lean feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms 2013-12-06 15:01:54 -08:00
t12.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
t13.lean fix(library/tactic/goal): to_goal way of handling context_entries of the form (name, domain, body) where domain is null, and body is a proof term 2013-12-06 16:14:25 -08:00
t13.lean.expected.out fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
test.sh fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00
test_single.sh fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 2013-12-06 17:03:12 -08:00