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

Replace subst overloading with interfaces too (mostly)

Browse source
This commit is contained in:
rhiannon morris 2023-02-20 22:22:23 +01:00
parent cb5bd6c98c
commit 1a7efc104e
6 changed files with 84 additions and 154 deletions
Download patch file Download diff file Expand all files Collapse all files

8
lib/Quox/Equal.idr
View file

@ -349,8 +349,8 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
defs <- ask
runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th =>
compare0 defs (map (/// th) ctx.tctx)
(ty /// th) (s /// th) (t /// th)
compare0 defs (map (// th) ctx.tctx)
(ty // th) (s // th) (t // th)
export covering
compareType : (s, t : Term q d n) -> m ()
@ -358,7 +358,7 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
defs <- ask
runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th =>
compareType defs (map (/// th) ctx.tctx) (s /// th) (t /// th)
compareType defs (map (// th) ctx.tctx) (s // th) (t // th)
namespace Elim
||| you don't have to pass the type in but the arguments must still be
@ -369,7 +369,7 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
defs <- ask
runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th =>
compare0 defs (map (/// th) ctx.tctx) (e /// th) (f /// th)
compare0 defs (map (// th) ctx.tctx) (e // th) (f // th)
namespace Term
export covering %inline