diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:36:35 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:36:35 +0000 |
| commit | 3b28f247fc97fa8ac543ad2b5f8026faad9c5173 (patch) | |
| tree | 5ebac6654e0b231d64af7fe47e86c8155fc075a7 | |
| parent | d22cbb0973b3f388e1092b1c1c4cd2d0f76d548e (diff) | |
Export properties of tmRel.
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 2013876..2712c88 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -34,6 +34,7 @@ bindTermsIsMap : {auto a : RawAlgebra sig} bindTermsIsMap env [] = Refl bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env t)) (bindTermsIsMap env ts) +-- FIXME: these names shouldn't be public. Indication of bad API design namespace Rel public export data (~=~) : forall v . (0 r : IRel v) -> IRel (Term sig v) @@ -47,8 +48,10 @@ namespace Rel -> Pointwise ((~=~) {sig} {v} r) tms tms' -> (~=~) {sig} {v} r t (Call op tms) (Call op tms') + public export tmRelEqualIsEqual : (~=~) (\_ => Equal) t tm tm' -> tm = tm' + public export tmsRelEqualIsEqual : Pointwise ((~=~) (\_ => Equal)) tms tms' -> tms = tms' tmRelEqualIsEqual (Done' eq) = cong Done eq @@ -57,9 +60,11 @@ namespace Rel tmsRelEqualIsEqual [] = Refl tmsRelEqualIsEqual (eq :: eqs) = cong2 (::) (tmRelEqualIsEqual eq) (tmsRelEqualIsEqual eqs) + public export tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel -> {t : sig.T} -> (tm : Term sig V t) -> (~=~) rel t tm tm + public export tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel -> {ts : List sig.T} -> (tms : Term sig V ^ ts) -> Pointwise ((~=~) rel) tms tms @@ -69,18 +74,22 @@ namespace Rel tmsRelRefl refl [] = [] tmsRelRefl refl (t :: ts) = tmRelRefl refl t :: tmsRelRefl refl ts + public export tmRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel -> {t : sig.T} -> {tm, tm' : Term sig V t} -> tm = tm' -> (~=~) rel t tm tm' tmRelReflexive refl Refl = tmRelRefl refl _ + public export tmsRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel -> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts} -> tms = tms' -> Pointwise ((~=~) rel) tms tms' tmsRelReflexive refl Refl = tmsRelRefl refl _ + public export tmRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel) -> {t : sig.T} -> {tm, tm' : Term sig V t} -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm + public export tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel) -> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts} -> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms @@ -91,10 +100,12 @@ namespace Rel tmsRelSym sym [] = [] tmsRelSym sym (t :: ts) = tmRelSym sym t :: tmsRelSym sym ts + public export tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel) -> {t : sig.T} -> {tm, tm', tm'' : Term sig V t} -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm'' -> (~=~) rel t tm tm'' + public export tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel) -> {ts : List sig.T} -> {tms, tms', tms'' : Term sig V ^ ts} -> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms'' |