diff options
Diffstat (limited to 'src/Soat/FirstOrder')
| -rw-r--r-- | src/Soat/FirstOrder/Algebra.idr | 8 | ||||
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 12 |
2 files changed, 10 insertions, 10 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr index fef5871..5f166d5 100644 --- a/src/Soat/FirstOrder/Algebra.idr +++ b/src/Soat/FirstOrder/Algebra.idr @@ -30,8 +30,8 @@ MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o)) public export record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where constructor MkIsAlgebra - 0 equivalence : IEquivalence a.U rel - 0 semCong : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity} + equivalence : IEquivalence a.U rel + semCong : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity} -> Pointwise rel tms tms' -> rel t (a.sem op tms) (a.sem op tms') public export @@ -51,8 +51,8 @@ record IsHomomorphism (f : (t : sig.T) -> a.raw.U t -> b.raw.U t) where constructor MkIsHomomorphism - 0 cong : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel t (f t tm) (f t tm') - 0 semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity) + cong : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel t (f t tm) (f t tm') + semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity) -> b.rel t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms)) public export diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 5f5e57b..af6539b 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -116,12 +116,12 @@ public export FreeAlgebra : ISetoid sig.T -> Algebra sig FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v) -public export 0 +public export bindTermCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid) -> {t : sig.T} -> {tm, tm' : Term sig x.U t} -> (~=~) x.relation t tm tm' -> a.rel t (bindTerm {a = a.raw} env.f tm) (bindTerm {a = a.raw} env.f tm') -public export 0 +public export bindTermsCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid) -> {ts : List sig.T} -> {tms, tms' : Term sig x.U ^ ts} -> Pointwise ((~=~) x.relation) tms tms' -> Pointwise a.rel (bindTerms {a = a.raw} env.f tms) (bindTerms {a = a.raw} env.f tms') @@ -148,15 +148,15 @@ public export bind : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) -> Homomorphism (FreeAlgebra v) a bind env = MkHomomorphism _ (bindHomo _ env) -public export 0 -bindUnique : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) +public export +bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) -> (f : Homomorphism (FreeAlgebra v) a) -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i)) -> {t : sig.T} -> (tm : Term sig v.U t) -> a.rel t (f.f t tm) ((Term.bind {a = a} env).f t tm) -public export 0 -bindsUnique : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) +public export +bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) -> (f : Homomorphism (FreeAlgebra v) a) -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i)) -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) |