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

refactor(library): move more notation to general_notation

Browse source
This commit is contained in:
Jeremy Avigad 2014-08-28 16:13:04 -04:00 committed by Leonardo de Moura
parent b9628842cf
commit 1864fc2f6c
3 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/general_notation.lean
View file

@ -32,6 +32,9 @@ precedence `=`:50
precedence `≠`:50 precedence `≠`:50
precedence `rfl`:max -- shorthand for reflexivity precedence `rfl`:max -- shorthand for reflexivity
precedence `≈`:50 -- used for path in hott
precedence `∼`:50
precedence `⁻¹`:100 precedence `⁻¹`:100
precedence `⬝`:75 -- infixr precedence `⬝`:75 -- infixr
precedence `▸`:75 -- infixr precedence `▸`:75 -- infixr
@ -74,8 +77,6 @@ precedence `∪`:65
-- ### other symbols -- ### other symbols
-- uncomment when inductive type syntax has changed
precedence `|`:55 -- used for absolute value, subtypes, divisibility precedence `|`:55 -- used for absolute value, subtypes, divisibility
precedence `++`:65 -- list append precedence `++`:65 -- list append
precedence `::`:65 -- list cons precedence `::`:65 -- list cons

2
library/hott/equiv.lean
View file

@ -58,4 +58,4 @@ Equiv_rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
-- TODO: better symbol -- TODO: better symbol
infix `<~>`:25 := Equiv infix `<~>`:25 := Equiv
notation e `⁻¹`:75 := equiv_inv e notation e `⁻¹` := equiv_inv e

6
library/hott/path.lean
View file

@ -18,7 +18,7 @@ using function
inductive path {A : Type} (a : A) : A → Type := inductive path {A : Type} (a : A) : A → Type :=
idpath : path a a idpath : path a a
infix `≈`:50 := path infix `≈` := path
notation x `≈` y:50 `:>`:0 A:0 := @path A x y -- TODO: is this right? notation x `≈` y:50 `:>`:0 A:0 := @path A x y -- TODO: is this right?
notation `idp`:max := idpath _ -- TODO: can we / should we use `1`? notation `idp`:max := idpath _ -- TODO: can we / should we use `1`?
@ -206,7 +206,7 @@ abbreviation ap01 := ap
abbreviation pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type := abbreviation pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type :=
Πx : A, f x ≈ g x Πx : A, f x ≈ g x
infix `∼`:50 := pointwise_paths infix `∼` := pointwise_paths
definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ∼ g := definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ∼ g :=
λx, path.induction_on H idp λx, path.induction_on H idp
@ -691,4 +691,4 @@ Hint Rewrite
Ltac hott_simpl := Ltac hott_simpl :=
autorewrite with paths in * |- * ; auto with path_hints. autorewrite with paths in * |- * ; auto with path_hints.
-/ -/