Commit 2020-03-02 21:45 fe9d7ff4
View on Github →feat(tactic/nat_cases): a tactic to case bash inequalities on natural numbers (#1596)
- starting on finset_cases
- looking pretty nice
- moving lemma that rewrites nat.add back to (+)
- update tactics.md
- cleanup
- suggestions from review
- Update src/tactic/fin_cases.lean Co-Authored-By: semorrison scott@tqft.net
- incomplete implementation of
withsyntax - looks good
- failed attempt to use unification
- test showing elaboration problem
- elaborating the
withargument with respect to the expected type - testing the type of A in
x ∈ Ausing unification rather than syntactic matching - refactor and cleanup
- refactor
- initial start on nat_cases
- initial start on nat_cases
- resuming work on nat_cases
- looks reasonable
- documentation
- reverting bad merge in fin_cases
- fix module comment
- move non-meta lemmas
- add tests for Chris' use case
- cleanup
- oops
- starting on fintype instances for Icos
- finishing fintypes
- minor
- not really sure what to do next
- oops, forgot to commit??
- oops
- bit more work
- more progress
- everything works?
- moving everything to their natural homes
- rearrange
- cleanup
- linting
- doc-strings
- merge two interactive tactics, via
usingkeyword - improve documentation, in response to review
- add interval_cases to tactic.default
- Apply suggestions from code review