chore: add Or.elim for tutorial

This commit is contained in:
Leonardo de Moura 2021-08-24 14:11:18 -07:00
parent 82eb1b3558
commit 63b11368ca

View file

@ -148,6 +148,11 @@ theorem Or.intro_left (b : Prop) (h : a) : Or a b :=
theorem Or.intro_right (a : Prop) (h : b) : Or a b :=
Or.inr h
theorem Or.elim {c : Prop} (h : Or a b) (left : a → c) (right : b → c) : c :=
match h with
| Or.inl h => left h
| Or.inr h => right h
inductive Bool : Type where
| false : Bool
| true : Bool