max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/sigma_lex): closes #1091

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-02 15:53:35 -07:00
parent 112aae2928
commit 9ebcd9c2ff
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/sigma_lex.lean
View file

@ -14,8 +14,8 @@ section
-- Lexicographical order based on Ra and Rb
inductive lex : sigma B → sigma B → Prop :=
| left : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
| right : ∀a {b₁ b₂}, Rb a b₁ b₂ → lex ⟨a, b₁⟩ ⟨a, b₂⟩
| left : ∀ {a₁ : A} (b₁ : B a₁) {a₂ : A} (b₂ : B a₂), Ra a₁ a₂ → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
| right : ∀ (a : A) {b₁ b₂ : B a}, Rb a b₁ b₂ → lex ⟨a, b₁⟩ ⟨a, b₂⟩
end