From cba6dafc58fd41578a220063f64e12752d970502 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 19 Feb 2023 17:00:51 +0100 Subject: [PATCH] remove unused confusing ClashE --- lib/Quox/Equal.idr | 5 ----- 1 file changed, 5 deletions(-) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index de4d7bb..fa704bb 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -8,11 +8,6 @@ import public Control.Monad.Reader import Data.Maybe -private %inline -ClashE : EqMode -> Term q d n -> Elim q d n -> Elim q d n -> Error q -ClashE mode ty = ClashT mode ty `on` E - - public export record Env where constructor MakeEnv