9 lines
115 B
Text
9 lines
115 B
Text
|
|
definition p1 := (10, 20, 30)
|
|
|
|
definition v2 : nat :=
|
|
match p1 with
|
|
⟨a, b⟩ := a
|
|
end
|
|
|
|
example : v2 = 10 := rfl
|