noncomputable def Blaster.decide' (c : Prop) : Bool

Equations

• Blaster.decide' c = match Classical.propDecidable c with | isTrue h => true | isFalse h => false

theorem Blaster.decide'_true (c : Prop) : Blaster.decide' c = true ↔ c

theorem Blaster.decide'_false (c : Prop) : Blaster.decide' c = false ↔ ¬c

noncomputable def Blaster.ite' {α : Sort u} (p : Prop) (x y : α) : α

Similar to ite but ignores decidable instance.

Equations

• Blaster.ite' p x y = match Blaster.decide' p with | true => x | false => y

noncomputable def Blaster.dite' {α : Sort u} (p : Prop) (t : p → α) (e : ¬p → α) : α

Similar to dite but ignores decidable instance.

Equations

• Blaster.dite' p t e = match h : Blaster.decide' p with | true => t ⋯ | false => e ⋯

theorem Blaster.ite_equiv : @ite = fun (α : Sort u) (p : Prop) (x : Decidable p) => Blaster.ite' p

theorem Blaster.dite_equiv : @dite = fun (α : Sort u) (p : Prop) (x : Decidable p) => Blaster.dite' p

theorem Blaster.ite_to_dite'_equiv : @ite = fun (α : Sort u) (p : Prop) (_d : Decidable p) (x y : α) => Blaster.dite' p (fun (x_1 : p) => x) fun (x : ¬p) => y

theorem Blaster.decide'_equiv : decide = fun (p : Prop) (x : Decidable p) => Blaster.decide' p