From 244b33d7860645b7319cd41f42da8565e94a3fc8 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 17 Sep 2023 19:10:52 +0200 Subject: [PATCH] fix some comments --- lib/Quox/Equal.idr | 3 --- lib/Quox/Name.idr | 3 +-- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 7b47ae4..d220039 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -674,9 +674,6 @@ compareType defs ctx s t = do parameters (loc : Loc) (ctx : TyContext d n) - -- [todo] only split on the dvars that are actually used anywhere in - -- the calls to `splits` - parameters (mode : EqMode) private fromInner : Eff EqualInner a -> Eff Equal a diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr index a31560b..3d53754 100644 --- a/lib/Quox/Name.idr +++ b/lib/Quox/Name.idr @@ -178,8 +178,7 @@ mn base = do modifyAt GEN S pure $ MN base i -||| generate a fresh binding name with the given base and -||| (optionally) location `loc` +||| generate a fresh binding name with the given base and location `loc` export mnb : Has NameGen fs => PBaseName -> Loc -> Eff fs BindName mnb base loc = pure $ BN !(mn base) loc