max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: for induction q with Quot.ind issue

Browse source 
See
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Induction.20alternative.20name.20when.20using.20Quot.2Eind.3F
This commit is contained in:
Leonardo de Moura 2021-08-26 11:15:14 -07:00
parent 1aa274e5c0
commit b5a434d8a9
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lean/run/quotInd.lean Normal file
View file

@ -0,0 +1,3 @@
example (r : α → α → Prop) (q : Quot r) : False := by
induction q using Quot.ind with
| mk x => admit