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

add weakD

Browse source
This commit is contained in:
rhiannon morris 2023-03-25 20:48:49 +01:00
parent 100063ab91
commit ab82883214
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
lib/Quox/Syntax/Dim.idr
View file

@ -132,3 +132,8 @@ DecEq (Dim d) where
public export %inline public export %inline
BV : (i : Nat) -> (0 _ : LT i d) => Dim d BV : (i : Nat) -> (0 _ : LT i d) => Dim d
BV i = B $ V i BV i = B $ V i
export
weakD : {default 1 by : Nat} -> Dim d -> Dim (by + d)
weakD p = p // shift by