rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

add name to type arg in Context' and Telescope'

Browse source
This commit is contained in:
rhiannon morris 2021-12-23 15:54:16 +01:00
parent c75332be44
commit dbd0a3a451
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Quox/Context.idr
View file

@ -22,7 +22,7 @@ data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where
%name Telescope tel %name Telescope tel
public export public export
Telescope' : Type -> (from, to : Nat) -> Type Telescope' : (a : Type) -> (from, to : Nat) -> Type
Telescope' a = Telescope (\_ => a) Telescope' a = Telescope (\_ => a)
||| a global context is actually just a telescope over no existing bindings ||| 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 Context tm len = Telescope tm 0 len
public export public export
Context' : Type -> (len : Nat) -> Type Context' : (a : Type) -> (len : Nat) -> Type
Context' a = Context (\_ => a) Context' a = Context (\_ => a)