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

fix(builtin/kernel): add ascii notation for transitivity

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-18 20:56:35 -08:00
parent 32c5bc25e3
commit 2753a0ffc0
2 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/builtin/kernel.lean
View file

@ -156,6 +156,7 @@ theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a
theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
:= subst H1 H2 := subst H1 H2
infixl 100 >< : trans
infixl 100 ⋈ : trans infixl 100 ⋈ : trans
theorem ne_symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a theorem ne_symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a

BIN
src/builtin/obj/kernel.olean
View file

Binary file not shown.