From 8056f326d7b32e7f869648e8a9f227e1fa82a072 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 18 May 2015 20:11:02 -0400 Subject: [PATCH] feat(reserved_notation): make is_typeof parsing-only, add ^ to HoTT --- hott/init/reserved_notation.hlean | 3 ++- library/init/reserved_notation.lean | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean index a08fae263..abe7003d3 100644 --- a/hott/init/reserved_notation.hlean +++ b/hott/init/reserved_notation.hlean @@ -66,6 +66,7 @@ reserve infixl `div`:70 reserve infixl `mod`:70 reserve infixl `/`:70 reserve prefix `-`:100 +reserve infix `^`:80 reserve infix `<=`:50 reserve infix `≤`:50 @@ -93,7 +94,7 @@ reserve infixl `++`:65 reserve infixr `::`:65 -- 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 `(` t `:` T `)` := is_typeof T t diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index b08af371c..6ded1f13f 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -95,7 +95,7 @@ reserve infixl `++`:65 reserve infixr `::`:65 -- 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 `(` t `:` T `)` := is_typeof T t