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

add Subst.one

Browse source
This commit is contained in:
rhiannon morris 2022-02-27 01:46:44 +01:00
parent 3ea9db1c82
commit 76c02adf03
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Quox/Syntax/Subst.idr
View file

@ -90,6 +90,11 @@ drop1 (Shift by) = Shift $ drop1 by
drop1 (t ::: th) = th drop1 (t ::: th) = th
public export %inline
one : f n -> Subst f (S n) n
one x = x ::: id
||| `prettySubst pr names bnd op cl th` pretty-prints the substitution `th`, ||| `prettySubst pr names bnd op cl th` pretty-prints the substitution `th`,
||| with the following arguments: ||| with the following arguments:
||| |||