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

test: pattern confusion example

Browse source 
cc @dselsam
This commit is contained in:
Leonardo de Moura 2019-12-19 13:32:57 -08:00
parent 57f6881c6c
commit f04f51a295
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
tests/elabissues/patternIssue.lean Normal file
View file

@ -0,0 +1,13 @@
inductive Moo : Type
| M1 : Moo
| M2 : Moo
inductive Foo : Type
| mk₁ : Moo → Foo
| mk₂ : Foo
def bar : Foo → String
| Foo.mk₁ M1 => "mk₁ M1"
| _ => "else"
#eval bar (Foo.mk₁ Moo.M2) -- "mk₁ M1"