forked from liamoc/holbert
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ROADMAP
23 lines (23 loc) · 870 Bytes
/
ROADMAP
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
- Multi-file documents (Yining)
- Imports
- Persistence to local storage
- Submission to server?
- Lockable regions
- Elimination rules and induction (Chris)
- Applying a rule as an elimination rule DONE
- Defining an inductive set
- Applying an induction tactic
- Simultaneous induction
- Defining inductive sets via grammar
- Equality and Definitions (Rayhana)
- Applying an equality rule as a rewrite DONE
- Definitions that are stricter than axioms.
- Transitive calculational proofs
- Inductive definitions (possibly)
- Syntax (Yueyang)
- Mix-fix definitions, parsing and pretty printing.
- Built-ins
- Strings
- Naturals
- Hidden premises
- e.g. a variable called "xs" in a rule implicity introduces a premise "xs List" but this is not usually displayed prominently and proofs attempt to solve it automatically.