michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/init/quot.lean): declare calc subst rule for iff

Browse source
This commit is contained in:
Jeremy Avigad 2015-09-24 23:38:20 -04:00 committed by Leonardo de Moura
parent 384a366e0f
commit 135f5ff96b
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/quot.lean
View file

@ -13,6 +13,10 @@ constant quot.{l} : Π {A : Type.{l}}, setoid A → Type.{l}
-- Remark: if we do not use propext here, then we would need a quot.lift for propositions. -- Remark: if we do not use propext here, then we would need a quot.lift for propositions.
constant propext {a b : Prop} : (a ↔ b) → a = b constant propext {a b : Prop} : (a ↔ b) → a = b
-- iff can now be used to do substitutions in a calculation
theorem iff_subst [subst] {a b : Prop} {P : Prop → Prop} (H₁ : a ↔ b) (H₂ : P a) : P b :=
eq.subst (propext H₁) H₂
namespace quot namespace quot
protected constant mk : Π {A : Type} [s : setoid A], A → quot s protected constant mk : Π {A : Type} [s : setoid A], A → quot s
notation `⟦`:max a `⟧`:0 := quot.mk a notation `⟦`:max a `⟧`:0 := quot.mk a