From dbd0a3a451bd98f451b2bc3307db333c8aa55ba8 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 23 Dec 2021 15:54:16 +0100 Subject: [PATCH] add name to type arg in Context' and Telescope' --- src/Quox/Context.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr index dc66a8b..25f151b 100644 --- a/src/Quox/Context.idr +++ b/src/Quox/Context.idr @@ -22,7 +22,7 @@ data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where %name Telescope tel public export -Telescope' : Type -> (from, to : Nat) -> Type +Telescope' : (a : Type) -> (from, to : Nat) -> Type Telescope' a = Telescope (\_ => a) ||| a global context is actually just a telescope over no existing bindings @@ -31,7 +31,7 @@ Context : (tm : Nat -> Type) -> (len : Nat) -> Type Context tm len = Telescope tm 0 len public export -Context' : Type -> (len : Nat) -> Type +Context' : (a : Type) -> (len : Nat) -> Type Context' a = Context (\_ => a)