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

add (?!) for nondependent contexts

Browse source
This commit is contained in:
rhiannon morris 2021-12-23 15:56:01 +01:00
parent 2a5b8ec815
commit 7bc58625a1
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Quox/Context.idr
View file

@ -75,6 +75,11 @@ public export %inline
(!!) : CanShift tm => Context tm len -> Var len -> tm len (!!) : CanShift tm => Context tm len -> Var len -> tm len
ctx !! i = getShift ctx i SZ ctx !! i = getShift ctx i SZ
infixl 8 !?
public export %inline
(!?) : Context' tm len -> Var len -> tm
ctx !? i = (ctx !! i) @{Const}
||| a triangle of bindings. each type binding in a context counts the ues of ||| a triangle of bindings. each type binding in a context counts the ues of
||| others in its type, and all of these together form a triangle. ||| others in its type, and all of these together form a triangle.

4
src/Quox/Syntax/Shift.idr
View file

@ -204,3 +204,7 @@ interface CanShift f where
(//) : f from -> Shift from to -> f to (//) : f from -> Shift from to -> f to
export CanShift Var where i // by = shift by i export CanShift Var where i // by = shift by i
namespace CanShift
export
[Const] CanShift (\_ => a) where x // _ = x