We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent d097609 commit 486ce90Copy full SHA for 486ce90
README.md
@@ -7,8 +7,9 @@ This library implements generalised rewriting based on the Coq approach and the
7
- [x] Constraint generation
8
- [x] generate the same constraints coq does
9
- [x] compare algorithm and constraints of the coq and the paper version
10
-- [ ]
+- [ ] Proof search
11
- [x] recreate eauto efficiently to handle multiple related goals
12
- - [ ] support adding tactics and theorems dynamically
+ - [x] support adding theorems dynamically
13
+ - [ ] support adding tactics dynamically
14
- [ ] solve real-world grw problems
15
- [ ] idris port
grw.pdf
-393 KB
0 commit comments