quox/lib/Quox/Equal.idr

462 lines
17 KiB
Idris
Raw Normal View History

2022-02-26 20:18:16 -05:00
module Quox.Equal
import Quox.BoolExtra
import public Quox.Typing
import public Control.Monad.Either
import public Control.Monad.Reader
import Data.Maybe
2022-02-26 20:18:16 -05:00
public export
2023-02-19 11:02:13 -05:00
record CmpContext where
constructor MkCmpContext
2023-01-08 08:59:25 -05:00
mode : EqMode
2023-01-08 14:44:25 -05:00
public export
2023-02-19 11:02:13 -05:00
0 HasCmpContext : (Type -> Type) -> Type
HasCmpContext = MonadReader CmpContext
2023-01-08 14:44:25 -05:00
public export
0 CanEqual : (q : Type) -> (Type -> Type) -> Type
2023-02-19 11:02:13 -05:00
CanEqual q m = (HasErr q m, HasCmpContext m)
2023-01-08 14:44:25 -05:00
private %inline
2023-02-19 11:02:13 -05:00
mode : HasCmpContext m => m EqMode
2023-01-08 14:44:25 -05:00
mode = asks mode
parameters {auto _ : CanEqual q m} (ctx : EqContext q n)
private %inline
clashT : Term q 0 n -> Term q 0 n -> Term q 0 n -> m a
clashT ty s t = throwError $ ClashT ctx !mode ty s t
2023-01-08 14:44:25 -05:00
private %inline
clashTy : Term q 0 n -> Term q 0 n -> m a
clashTy s t = throwError $ ClashTy ctx !mode s t
private %inline
clashE : Elim q 0 n -> Elim q 0 n -> m a
clashE e f = throwError $ ClashE ctx !mode e f
2023-01-08 14:44:25 -05:00
2023-02-19 11:04:57 -05:00
||| true if a term is syntactically a type, or is neutral.
|||
||| this function *doesn't* push substitutions, because its main use is as a
||| `So` argument to skip cases that are already known to be nonsense. and
||| the substitutions have already been pushed.
2023-02-10 15:40:44 -05:00
public export %inline
2023-02-11 12:15:50 -05:00
isTyCon : (t : Term {}) -> Bool
isTyCon (TYPE {}) = True
isTyCon (Pi {}) = True
isTyCon (Lam {}) = False
isTyCon (Sig {}) = True
isTyCon (Pair {}) = False
isTyCon (Enum {}) = True
isTyCon (Tag {}) = False
2023-02-11 12:15:50 -05:00
isTyCon (Eq {}) = True
isTyCon (DLam {}) = False
isTyCon (E {}) = True
isTyCon (CloT {}) = False
isTyCon (DCloT {}) = False
2023-02-12 15:30:08 -05:00
public export %inline
sameTyCon : (s, t : Term q d n) ->
(0 ts : So (isTyCon s)) => (0 tt : So (isTyCon t)) =>
Bool
sameTyCon (TYPE {}) (TYPE {}) = True
sameTyCon (TYPE {}) _ = False
sameTyCon (Pi {}) (Pi {}) = True
sameTyCon (Pi {}) _ = False
sameTyCon (Sig {}) (Sig {}) = True
sameTyCon (Sig {}) _ = False
sameTyCon (Enum {}) (Enum {}) = True
sameTyCon (Enum {}) _ = False
2023-02-12 15:30:08 -05:00
sameTyCon (Eq {}) (Eq {}) = True
sameTyCon (Eq {}) _ = False
sameTyCon (E {}) (E {}) = True
sameTyCon (E {}) _ = False
parameters (defs : Definitions' q g)
2023-02-19 11:04:57 -05:00
||| true if a type is known to be a subsingleton purely by its form.
||| a subsingleton is a type with only zero or one possible values.
||| equality/subtyping accepts immediately on values of subsingleton types.
|||
||| * a function type is a subsingleton if its codomain is.
||| * a pair type is a subsingleton if both its elements are.
||| * all equality types are subsingletons because uip is admissible by
||| boundary separation.
||| * an enum type is a subsingleton if it has zero or one tags.
2023-02-19 11:43:27 -05:00
public export
isSubSing : HasErr q m => Term q 0 n -> m Bool
isSubSing ty = do
Element ty nc <- whnfT defs ty
2023-02-12 15:30:08 -05:00
case ty of
TYPE _ => pure False
2023-02-22 01:40:19 -05:00
Pi {res, _} => isSubSing res.term
Lam {} => pure False
2023-03-03 06:19:15 -05:00
Sig {fst, snd} => isSubSing fst `andM` isSubSing snd.term
Pair {} => pure False
Enum tags => pure $ length (SortedSet.toList tags) <= 1
Tag {} => pure False
Eq {} => pure True
DLam {} => pure False
2023-02-22 01:40:19 -05:00
E (s :# _) => isSubSing s
E _ => pure False
2023-02-10 15:40:44 -05:00
2023-03-15 10:54:51 -04:00
export
ensureTyCon : HasErr q m =>
(ctx : EqContext q n) -> (t : Term q 0 n) -> m (So (isTyCon t))
ensureTyCon ctx t = case nchoose $ isTyCon t of
Left y => pure y
Right n => throwError $ NotType (toTyContext ctx) (t // shift0 ctx.dimLen)
parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
mutual
namespace Term
2023-02-19 11:04:57 -05:00
||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to
||| the current variance `mode`.
|||
||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
2023-02-10 15:40:44 -05:00
export covering %inline
compare0 : EqContext q n -> (ty, s, t : Term q 0 n) -> m ()
2023-02-19 11:54:39 -05:00
compare0 ctx ty s t =
wrapErr (WhileComparingT ctx !mode ty s t) $ do
Element ty nty <- whnfT defs ty
Element s ns <- whnfT defs s
Element t nt <- whnfT defs t
tty <- ensureTyCon ctx ty
2023-02-19 11:54:39 -05:00
compare0' ctx ty s t
2023-02-10 15:40:44 -05:00
2023-02-19 11:04:57 -05:00
||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with
||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t".
2023-02-10 15:40:44 -05:00
private %inline
toLamBody : Elim q d n -> Term q d (S n)
toLamBody e = E $ weakE e :@ BVT 0
private covering
compare0' : EqContext q n ->
2023-02-10 15:40:44 -05:00
(ty, s, t : Term q 0 n) ->
2023-02-11 12:15:50 -05:00
(0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) =>
2023-02-10 15:40:44 -05:00
(0 ns : NotRedex defs s) => (0 nt : NotRedex defs t) =>
m ()
2023-02-10 15:40:44 -05:00
compare0' ctx (TYPE _) s t = compareType ctx s t
2023-03-15 10:54:51 -04:00
compare0' ctx ty@(Pi {qty, arg, res}) s t {n} = local {mode := Equal} $
2023-02-10 15:40:44 -05:00
case (s, t) of
2023-03-15 10:54:51 -04:00
-- Γ, x : A ⊢ s = t : B
-- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
2023-02-22 01:40:19 -05:00
(Lam b1, Lam b2) => compare0 ctx' res.term b1.term b2.term
2023-02-19 11:04:57 -05:00
-- Γ, x : A ⊢ s = e x : B
2023-03-15 10:54:51 -04:00
-- -----------------------------------
-- Γ ⊢ (λ x ⇒ s) = e : (π·x : A) → B
2023-02-22 01:40:19 -05:00
(E e, Lam b) => eta e b
(Lam b, E e) => eta e b
2023-02-19 11:04:57 -05:00
(E e, E f) => Elim.compare0 ctx e f
2023-03-15 10:54:51 -04:00
(Lam _, t) => throwError $ WrongType ctx ty t
(E _, t) => throwError $ WrongType ctx ty t
(s, _) => throwError $ WrongType ctx ty s
2023-02-19 11:04:57 -05:00
where
ctx' : EqContext q (S n)
2023-03-15 10:54:51 -04:00
ctx' = extendTy qty res.name arg ctx
2023-02-19 11:04:57 -05:00
eta : Elim q 0 n -> ScopeTerm q 0 n -> m ()
2023-02-22 01:40:19 -05:00
eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
eta e (S _ (N _)) = clashT ctx ty s t
2023-02-10 15:40:44 -05:00
compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
case (s, t) of
2023-02-19 11:04:57 -05:00
-- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x}
2023-03-15 10:54:51 -04:00
-- --------------------------------------------
-- Γ ⊢ (s₁, t₁) = (s₂,t₂) : (x : A) × B
2023-02-19 11:04:57 -05:00
--
-- [todo] η for π ≥ 0 maybe
2023-02-10 15:40:44 -05:00
(Pair sFst sSnd, Pair tFst tSnd) => do
compare0 ctx fst sFst tFst
compare0 ctx (sub1 snd (sFst :# fst)) sSnd tSnd
2023-02-19 11:04:57 -05:00
2023-03-15 10:54:51 -04:00
(E e, E f) => Elim.compare0 ctx e f
(Pair {}, t) => throwError $ WrongType ctx ty t
(E _, t) => throwError $ WrongType ctx ty t
(s, _) => throwError $ WrongType ctx ty s
2023-02-10 15:40:44 -05:00
compare0' ctx ty@(Enum tags) s t = local {mode := Equal} $
case (s, t) of
-- --------------------
-- Γ ⊢ `t = `t : {ts}
--
-- t ∈ ts is in the typechecker, not here, ofc
(Tag t1, Tag t2) => unless (t1 == t2) $ clashT ctx ty s t
2023-03-15 10:54:51 -04:00
(E e, E f) => Elim.compare0 ctx e f
(Tag _, t) => throwError $ WrongType ctx ty t
(E _, t) => throwError $ WrongType ctx ty t
(s, _) => throwError $ WrongType ctx ty s
2023-02-19 11:04:57 -05:00
compare0' _ (Eq {}) _ _ =
-- ✨ uip ✨
--
-- Γ ⊢ e = f : Eq [i ⇒ A] s t
pure ()
2023-02-10 15:40:44 -05:00
compare0' ctx ty@(E _) s t = do
-- a neutral type can only be inhabited by neutral values
-- e.g. an abstract value in an abstract type, bound variables, …
2023-03-15 10:54:51 -04:00
E e <- pure s | _ => throwError $ WrongType ctx ty s
E f <- pure t | _ => throwError $ WrongType ctx ty t
2023-02-12 15:30:08 -05:00
Elim.compare0 ctx e f
2023-02-10 15:40:44 -05:00
2023-02-19 11:04:57 -05:00
||| compares two types, using the current variance `mode` for universes.
||| fails if they are not types, even if they would happen to be equal.
2023-02-19 11:43:14 -05:00
export covering %inline
compareType : EqContext q n -> (s, t : Term q 0 n) -> m ()
2023-02-10 15:40:44 -05:00
compareType ctx s t = do
Element s ns <- whnfT defs s
Element t nt <- whnfT defs t
ts <- ensureTyCon ctx s
tt <- ensureTyCon ctx t
st <- either pure (const $ clashTy ctx s t) $
2023-02-12 15:30:08 -05:00
nchoose $ sameTyCon s t
2023-02-10 15:40:44 -05:00
compareType' ctx s t
private covering
compareType' : EqContext q n -> (s, t : Term q 0 n) ->
2023-02-11 12:15:50 -05:00
(0 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) =>
(0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) =>
2023-02-12 15:30:08 -05:00
(0 st : So (sameTyCon s t)) =>
2023-02-10 15:40:44 -05:00
m ()
2023-02-19 11:04:57 -05:00
-- equality is the same as subtyping, except with the
-- "≤" in the TYPE rule being replaced with "="
2023-02-12 15:30:08 -05:00
compareType' ctx (TYPE k) (TYPE l) =
2023-02-19 11:04:57 -05:00
-- 𝓀
-- ----------------------
-- Γ ⊢ Type 𝓀 <: Type
2023-02-12 15:30:08 -05:00
expectModeU !mode k l
compareType' ctx (Pi {qty = sQty, arg = sArg, res = sRes, _})
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
2023-02-19 11:04:57 -05:00
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
-- ----------------------------------------
-- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
2023-02-12 15:30:08 -05:00
expectEqualQ sQty tQty
local {mode $= flip} $ compareType ctx sArg tArg -- contra
2023-03-15 10:54:51 -04:00
compareType (extendTy zero sRes.name sArg ctx) sRes.term tRes.term
2023-02-12 15:30:08 -05:00
compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
(Sig {fst = tFst, snd = tSnd, _}) = do
2023-02-19 11:04:57 -05:00
-- Γ ⊢ A₁ <: A₂ Γ, x : A₁ ⊢ B₁ <: B₂
-- --------------------------------------
-- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂
2023-02-12 15:30:08 -05:00
compareType ctx sFst tFst
2023-03-15 10:54:51 -04:00
compareType (extendTy zero sSnd.name sFst ctx) sSnd.term tSnd.term
2023-02-12 15:30:08 -05:00
compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
(Eq {ty = tTy, l = tl, r = tr, _}) = do
2023-02-19 11:04:57 -05:00
-- Γ ⊢ A₁ε/i <: A₂ε/i
-- Γ ⊢ l₁ = l₂ : A₁𝟎/i Γ ⊢ r₁ = r₂ : A₁𝟏/i
-- ------------------------------------------------
-- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
compareType (extendDim sTy.name One ctx) sTy.one tTy.one
2023-02-12 15:30:08 -05:00
local {mode := Equal} $ do
Term.compare0 ctx sTy.zero sl tl
Term.compare0 ctx sTy.one sr tr
compareType' ctx s@(Enum tags1) t@(Enum tags2) = do
-- ------------------
-- Γ ⊢ {ts} <: {ts}
--
-- no subtyping based on tag subsets, since that would need
-- a runtime coercion
unless (tags1 == tags2) $ clashTy ctx s t
2023-02-12 15:30:08 -05:00
compareType' ctx (E e) (E f) = do
-- no fanciness needed here cos anything other than a neutral
-- has been inlined by whnf
2023-02-12 15:30:08 -05:00
Elim.compare0 ctx e f
2023-02-11 12:15:50 -05:00
2023-02-19 11:04:57 -05:00
||| performs the minimum work required to recompute the type of an elim.
|||
||| ⚠ **assumes the elim is already typechecked.** ⚠
2023-02-11 12:15:50 -05:00
private covering
computeElimType : EqContext q n -> (e : Elim q 0 n) ->
2023-02-12 15:30:08 -05:00
(0 ne : NotRedex defs e) ->
2023-02-11 12:15:50 -05:00
m (Term q 0 n)
2023-02-12 15:30:08 -05:00
computeElimType ctx (F x) _ = do
2023-02-11 12:15:50 -05:00
defs <- lookupFree' defs x
pure $ defs.type.get
2023-02-12 15:30:08 -05:00
computeElimType ctx (B i) _ = do
pure $ ctx.tctx !! i
2023-02-12 15:30:08 -05:00
computeElimType ctx (f :@ s) ne = do
(_, arg, res) <- expectPiE defs ctx !(computeElimType ctx f (noOr1 ne))
2023-02-11 12:15:50 -05:00
pure $ sub1 res (s :# arg)
2023-02-12 15:30:08 -05:00
computeElimType ctx (CasePair {pair, ret, _}) _ = do
2023-02-11 12:15:50 -05:00
pure $ sub1 ret pair
computeElimType ctx (CaseEnum {tag, ret, _}) _ = do
pure $ sub1 ret tag
2023-02-12 15:30:08 -05:00
computeElimType ctx (f :% p) ne = do
(ty, _, _) <- expectEqE defs ctx !(computeElimType ctx f (noOr1 ne))
2023-02-11 12:15:50 -05:00
pure $ dsub1 ty p
2023-02-12 15:30:08 -05:00
computeElimType ctx (_ :# ty) _ = do
2023-02-11 12:15:50 -05:00
pure ty
private covering
replaceEnd : EqContext q n ->
2023-02-11 12:15:50 -05:00
(e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
m (Elim q 0 n)
replaceEnd ctx e p ne = do
(ty, l, r) <- expectEqE defs ctx !(computeElimType ctx e ne)
2023-02-11 12:15:50 -05:00
pure $ ends l r p :# dsub1 ty (K p)
namespace Elim
2023-02-11 12:15:50 -05:00
-- [fixme] the following code ends up repeating a lot of work in the
-- computeElimType calls. the results should be shared better
2023-02-19 11:04:57 -05:00
||| compare two eliminations according to the given variance `mode`.
|||
||| ⚠ **assumes that they have both been typechecked, and have
||| equal types.** ⚠
2023-02-10 15:40:44 -05:00
export covering %inline
compare0 : EqContext q n -> (e, f : Elim q 0 n) -> m ()
2023-02-10 15:40:44 -05:00
compare0 ctx e f =
wrapErr (WhileComparingE ctx !mode e f) $ do
Element e ne <- whnfT defs e
Element f nf <- whnfT defs f
2023-02-19 11:54:39 -05:00
-- [fixme] there is a better way to do this "isSubSing" stuff for sure
unless !(isSubSing defs !(computeElimType ctx e ne)) $
2023-02-19 11:54:39 -05:00
compare0' ctx e f ne nf
2023-02-10 15:40:44 -05:00
private covering
compare0' : EqContext q n ->
(e, f : Elim q 0 n) ->
2023-02-12 15:30:08 -05:00
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
2023-02-11 12:15:50 -05:00
m ()
-- replace applied equalities with the appropriate end first
2023-02-12 15:30:08 -05:00
-- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A𝟎/i
2023-02-19 11:04:57 -05:00
--
-- [todo] maybe have typed whnf and do this (and η???) there instead
2023-02-12 15:30:08 -05:00
compare0' ctx (e :% K p) f ne nf =
2023-02-11 12:15:50 -05:00
compare0 ctx !(replaceEnd ctx e p $ noOr1 ne) f
2023-02-12 15:30:08 -05:00
compare0' ctx e (f :% K q) ne nf =
2023-02-11 12:15:50 -05:00
compare0 ctx e !(replaceEnd ctx f q $ noOr1 nf)
compare0' ctx e@(F x) f@(F y) _ _ = unless (x == y) $ clashE ctx e f
compare0' ctx e@(F _) f _ _ = clashE ctx e f
2023-02-10 15:40:44 -05:00
compare0' ctx e@(B i) f@(B j) _ _ = unless (i == j) $ clashE ctx e f
compare0' ctx e@(B _) f _ _ = clashE ctx e f
2023-02-10 15:40:44 -05:00
2023-02-12 15:30:08 -05:00
compare0' ctx (e :@ s) (f :@ t) ne nf =
local {mode := Equal} $ do
compare0 ctx e f
(_, arg, _) <- expectPiE defs ctx !(computeElimType ctx e (noOr1 ne))
2023-02-12 15:30:08 -05:00
Term.compare0 ctx arg s t
compare0' ctx e@(_ :@ _) f _ _ = clashE ctx e f
2023-02-10 15:40:44 -05:00
2023-02-22 01:40:19 -05:00
compare0' ctx (CasePair epi e eret ebody)
(CasePair fpi f fret fbody) ne nf =
local {mode := Equal} $ do
2023-02-11 12:15:50 -05:00
compare0 ctx e f
2023-02-12 15:30:08 -05:00
ety <- computeElimType ctx e (noOr1 ne)
2023-03-15 10:54:51 -04:00
compareType (extendTy zero eret.name ety ctx) eret.term fret.term
(fst, snd) <- expectSigE defs ctx ety
let [< x, y] = ebody.names
2023-03-15 10:54:51 -04:00
Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
(substCasePairRet ety eret)
ebody.term fbody.term
expectEqualQ epi fpi
compare0' ctx e@(CasePair {}) f _ _ = clashE ctx e f
2023-02-10 15:40:44 -05:00
compare0' ctx (CaseEnum epi e eret earms)
(CaseEnum fpi f fret farms) ne nf =
local {mode := Equal} $ do
compare0 ctx e f
ety <- computeElimType ctx e (noOr1 ne)
2023-03-15 10:54:51 -04:00
compareType (extendTy zero eret.name ety ctx) eret.term fret.term
for_ !(expectEnumE defs ctx ety) $ \t =>
compare0 ctx (sub1 eret $ Tag t :# ety)
!(lookupArm t earms) !(lookupArm t farms)
expectEqualQ epi fpi
where
lookupArm : TagVal -> CaseEnumArms q d n -> m (Term q d n)
lookupArm t arms = case lookup t arms of
Just arm => pure arm
Nothing => throwError $ TagNotIn t (fromList $ keys arms)
compare0' ctx e@(CaseEnum {}) f _ _ = clashE ctx e f
2023-02-22 01:40:19 -05:00
compare0' ctx (s :# a) (t :# b) _ _ =
Term.compare0 ctx !(bigger a b) s t
where
bigger : forall a. a -> a -> m a
bigger l r = asks mode <&> \case Super => l; _ => r
2023-02-12 15:30:08 -05:00
compare0' ctx (s :# a) f _ _ = Term.compare0 ctx a s (E f)
compare0' ctx e (t :# b) _ _ = Term.compare0 ctx b (E e) t
compare0' ctx e@(_ :# _) f _ _ = clashE ctx e f
2023-02-10 15:40:44 -05:00
2023-03-15 10:54:51 -04:00
parameters {auto _ : (HasDefs' q _ m, HasErr q m, IsQty q)}
(ctx : TyContext q d n)
-- [todo] only split on the dvars that are actually used anywhere in
-- the calls to `splits`
2023-02-10 15:40:44 -05:00
parameters (mode : EqMode)
namespace Term
2023-02-10 15:40:44 -05:00
export covering
compare : (ty, s, t : Term q d n) -> m ()
compare ty s t = do
defs <- ask
2023-02-19 11:02:13 -05:00
runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th =>
let ectx = makeEqContext ctx th in
compare0 defs ectx (ty // th) (s // th) (t // th)
2023-02-10 15:40:44 -05:00
export covering
compareType : (s, t : Term q d n) -> m ()
compareType s t = do
defs <- ask
2023-02-19 11:02:13 -05:00
runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th =>
let ectx = makeEqContext ctx th in
compareType defs ectx (s // th) (t // th)
namespace Elim
2023-02-11 12:15:50 -05:00
||| you don't have to pass the type in but the arguments must still be
||| of the same type!!
export covering %inline
2023-02-10 15:40:44 -05:00
compare : (e, f : Elim q d n) -> m ()
compare e f = do
defs <- ask
2023-02-19 11:02:13 -05:00
runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th =>
let ectx = makeEqContext ctx th in
compare0 defs ectx (e // th) (f // th)
namespace Term
export covering %inline
2023-02-14 16:29:06 -05:00
equal, sub, super : (ty, s, t : Term q d n) -> m ()
2023-02-10 15:40:44 -05:00
equal = compare Equal
sub = compare Sub
2023-02-14 16:29:06 -05:00
super = compare Super
export covering %inline
2023-02-14 16:29:06 -05:00
equalType, subtype, supertype : (s, t : Term q d n) -> m ()
2023-02-10 15:40:44 -05:00
equalType = compareType Equal
subtype = compareType Sub
2023-02-14 16:29:06 -05:00
supertype = compareType Super
namespace Elim
export covering %inline
2023-02-14 16:29:06 -05:00
equal, sub, super : (e, f : Elim q d n) -> m ()
2023-02-10 15:40:44 -05:00
equal = compare Equal
sub = compare Sub
2023-02-14 16:29:06 -05:00
super = compare Super