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

feat(reserved_notation): make is_typeof parsing-only, add ^ to HoTT

Browse source
This commit is contained in:
Floris van Doorn 2015-05-18 20:11:02 -04:00 committed by Leonardo de Moura
parent 0c7e16e017
commit 8056f326d7
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
hott/init/reserved_notation.hlean
View file

@ -66,6 +66,7 @@ reserve infixl `div`:70
reserve infixl `mod`:70 reserve infixl `mod`:70
reserve infixl `/`:70 reserve infixl `/`:70
reserve prefix `-`:100 reserve prefix `-`:100
reserve infix `^`:80
reserve infix `<=`:50 reserve infix `<=`:50
reserve infix `≤`:50 reserve infix `≤`:50
@ -93,7 +94,7 @@ reserve infixl `++`:65
reserve infixr `::`:65 reserve infixr `::`:65
-- Yet another trick to anotate an expression with a type -- Yet another trick to anotate an expression with a type
abbreviation is_typeof (A : Type) (a : A) : A := a abbreviation is_typeof [parsing-only] (A : Type) (a : A) : A := a
notation `typeof` t `:` T := is_typeof T t notation `typeof` t `:` T := is_typeof T t
notation `(` t `:` T `)` := is_typeof T t notation `(` t `:` T `)` := is_typeof T t

2
library/init/reserved_notation.lean
View file

@ -95,7 +95,7 @@ reserve infixl `++`:65
reserve infixr `::`:65 reserve infixr `::`:65
-- Yet another trick to anotate an expression with a type -- Yet another trick to anotate an expression with a type
abbreviation is_typeof (A : Type) (a : A) : A := a abbreviation is_typeof [parsing-only] (A : Type) (a : A) : A := a
notation `typeof` t `:` T := is_typeof T t notation `typeof` t `:` T := is_typeof T t
notation `(` t `:` T `)` := is_typeof T t notation `(` t `:` T `)` := is_typeof T t