From 63b11368cab0ff9e82744d5333e6493d76874b0a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Aug 2021 14:11:18 -0700 Subject: [PATCH] chore: add `Or.elim` for tutorial --- src/Init/Prelude.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 487a33bec8..88a7fed1e0 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -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