From cd82a24ca97ed336ec8eb8b40ba9531a2be8ad7e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Apr 2022 15:00:13 -0700 Subject: [PATCH] chore: avoid "denote" overloading It the overload does not affect elaboration, but pollutes the info view. --- doc/examples/phoas.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/examples/phoas.lean b/doc/examples/phoas.lean index 5f8413646e..019b6a985e 100644 --- a/doc/examples/phoas.lean +++ b/doc/examples/phoas.lean @@ -61,7 +61,8 @@ We write the final type of a closed term using polymorphic quantification over a choices of `rep` type family -/ -open Ty Term' +open Ty (nat fn) +open Term' namespace FirstTry