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

remove unused confusing ClashE

Browse source
This commit is contained in:
rhiannon morris 2023-02-19 17:00:51 +01:00
parent 9bfc82ca43
commit cba6dafc58
1 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
lib/Quox/Equal.idr
View file

@ -8,11 +8,6 @@ import public Control.Monad.Reader
import Data.Maybe 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 public export
record Env where record Env where
constructor MakeEnv constructor MakeEnv