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

fix an outdated comment

Browse source
This commit is contained in:
rhiannon morris 2021-11-21 14:59:41 +01:00
parent 37230a8032
commit fce293caa7
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -90,16 +90,14 @@ drop1 (Shift by) = Shift $ drop1 by
drop1 (t ::: th) = th drop1 (t ::: th) = th
||| `prettySubst pr bnd op cl unicode 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:
||| |||
||| * `th : Subst f from to` ||| * `th : Subst f from to`
||| * `pr : (unicode : Bool) -> f to -> m (Doc HL)` prints a single element ||| * `pr : f to -> m (Doc HL)` prints a single element
||| * `names : List Name` is a list of known bound var names ||| * `names : List Name` is a list of known bound var names
||| * `bnd : HL` is the highlight to use for bound variables being subsituted ||| * `bnd : HL` is the highlight to use for bound variables being subsituted
||| * `op, cl : Doc HL` are the opening and closing brackets ||| * `op, cl : Doc HL` are the opening and closing brackets
||| * `unicode : Bool` is whether to use unicode characters in the output
||| (also passed into `pr`)
export export
prettySubstM : Pretty.HasEnv m => prettySubstM : Pretty.HasEnv m =>
(pr : f to -> m (Doc HL)) -> (pr : f to -> m (Doc HL)) ->