13 lines
214 B
Text
13 lines
214 B
Text
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"
|