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

fix(library/init/sigma): make sure file compiles even when '--to_axiom' is used

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-16 12:52:08 -07:00
parent 0ae24faae3
commit b80a391d63
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/sigma.lean
View file

@ -28,7 +28,7 @@ namespace sigma
variable (Rb : ∀ a, B a → B a → Prop)
theorem dpair_eq : ∀ {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂), eq.rec_on H₁ b₁ = b₂ → ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩
| a₁ a₁ b₁ b₁ rfl rfl := rfl
| a₁ a₁ b₁ b₁ (eq.refl a₁) (eq.refl b₁) := rfl
protected theorem eq {p₁ p₂ : Σa : A, B a} :
∀(H₁ : p₁.1 = p₂.1) (H₂ : eq.rec_on H₁ p₁.2 = p₂.2), p₁ = p₂ :=