diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr index 2658e0a..6035633 100644 --- a/src/Quox/Syntax/Subst.idr +++ b/src/Quox/Syntax/Subst.idr @@ -90,16 +90,14 @@ drop1 (Shift by) = Shift $ drop1 by 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: ||| ||| * `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 ||| * `bnd : HL` is the highlight to use for bound variables being subsituted ||| * `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 prettySubstM : Pretty.HasEnv m => (pr : f to -> m (Doc HL)) ->