mathlib3
feat(tactic/fin_cases): case bashing on finset, list, and fintype hypotheses.
#775
Merged
Merged
feat(tactic/fin_cases): case bashing on finset, list, and fintype hypotheses. #775
robertylewis
merged
18 commits into
leanprover-community:master
from
kim-em:finset_cases
starting on finset_cases
f75f3e47
looking pretty nice
94571a74
moving lemma that rewrites nat.add back to (+)
58e343a2
update tactics.md
2ed9ea5a
cleanup
261db39d
suggestions from review
8da35904
robertylewis
commented
on 2019-03-01
Update src/tactic/fin_cases.lean
b552dfe2
incomplete implementation of `with` syntax
f3439fff
johoelzl
commented
on 2019-03-01
almost there
a2d18b8f
looks good
cc8ecb78
failed attempt to use unification
e179e55c
robertylewis
commented
on 2019-03-02
test showing elaboration problem
3b3c9b71
elaborating the `with` argument with respect to the expected type
39e948c6
testing the type of A in `x ∈ A` using unification rather than syntac…
2f6fe760
refactor and cleanup
38bf2e16
refactor
d04e397d
feat(tactic/fin_cases): remove syntactic match
b168d73d
Merge pull request #1 from robertylewis/fin_cases
514a7d3f
Login to write a write a comment.
Login via GitHub