Issues
- 0
Consider using th-desugar
#11 opened by TOTBWF - 0
`auto` should use `induction`
#9 opened by TOTBWF - 1
Implement Extended Type Language
#10 opened by TOTBWF - 0
`apply` can't handle typeclass methods
#8 opened by TOTBWF - 2
- 0
Optional Subgoal Labels
#5 opened by TOTBWF - 0
Properly handle hypothesis name freshening
#6 opened by TOTBWF - 3
Implement Induction Tactic
#4 opened by TOTBWF - 3
The Tactic monad is non-associative
#2 opened by TOTBWF