aboutsummaryrefslogtreecommitdiff
path: root/spartan/core/goals.ML
diff options
context:
space:
mode:
authorJosh Chen2020-08-05 15:21:43 +0200
committerJosh Chen2020-08-05 15:21:43 +0200
commitc530305cbcafba9f66f1a55a1b5177a62f52535c (patch)
tree2c4736cf5884e53edd0b8eaebb903bb3f4857d2f /spartan/core/goals.ML
parent710f314a9ccb84cdd9df9bc8bf52482b8d1f5a56 (diff)
1. fix intros method. 2. Couple extra lemmas; good small test cases for normalization in typechecking/elaboration.
Diffstat (limited to 'spartan/core/goals.ML')
0 files changed, 0 insertions, 0 deletions