diff options
| -rw-r--r-- | README.md | 13 |
1 files changed, 7 insertions, 6 deletions
@@ -20,10 +20,11 @@ $ echo path/to/Isabelle/HoTT >> ~/.isabelle/Isabelle2020/ROOTS In no particular order. Some of the following might require changes to the Isabelle prover itself. -[ ] Typing information is implicit in context facts, and the collection must be searched every time we need a type for a term. - For performance, should probably implement dedicated tables. -[ ] Tactic-based term elaboration has (at least) two problems: 1. `assume(s)` clauses don't accept schematic vars, and 2. it often results in overly-flexible subgoals that the typechecker doesn't solve. - Will likely need an elaborator integrated into Isabelle's syntax checking. -[ ] Inductive type definitions. -[ ] Recursive function definitions. +- [ ] Implement dedicated tables for type information. +- [ ] Tactic-based term elaboration has (at least) two problems: + 1. `assume(s)` clauses don't accept schematic vars, and + 2. it often results in overly-flexible subgoals that the typechecker doesn't solve. + Will need an elaborator integrated into Isabelle's syntax checking. +- [ ] Inductive type definitions. +- [ ] Recursive function definitions. |