From 74b28f6ad9ca4de5022b4e8a05a49d559fbe512c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Mar 2015 18:35:21 -0700 Subject: [PATCH] feat(library,hott): new notation for typeof --- hott/init/reserved_notation.hlean | 1 + library/init/reserved_notation.lean | 1 + 2 files changed, 2 insertions(+) diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean index 741c6f9ad..a8f96c8f5 100644 --- a/hott/init/reserved_notation.hlean +++ b/hott/init/reserved_notation.hlean @@ -100,3 +100,4 @@ reserve infixr `::`:65 definition is_typeof (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 cb024df83..3c17d9d48 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -97,3 +97,4 @@ reserve infixr `::`:65 definition is_typeof (A : Type) (a : A) : A := a notation `typeof` t `:` T := is_typeof T t +notation `(` t `:` T `)` := is_typeof T t