From fcd024cb01e484dc3c92212f4317b254bbd7580b Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 6 Dec 2022 16:18:29 +0000 Subject: Add smart constructor for first-order algebras. --- src/Soat/FirstOrder/Term.idr | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'src/Soat/FirstOrder/Term.idr') diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 2042d2f..a53e6b0 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -105,17 +105,20 @@ namespace Rel , transitive = \t, x, y, z => tmRelTrans eq.transitive } + public export + Term : (0 sig : Signature) -> (V : IndexedSetoid sig.T) -> IndexedSetoid sig.T + Term sig v = MkIndexedSetoid (Term sig v.U) (tmRelEq v.equivalence) + public export Free : (0 V : sig.T -> Type) -> RawAlgebra sig Free v = MkRawAlgebra (Term sig v) Call -public export -FreeIsAlgebra : (v : IndexedSetoid sig.T) -> IsAlgebra sig (Free v.U) -FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call - public export FreeAlgebra : IndexedSetoid sig.T -> Algebra sig -FreeAlgebra v = MkAlgebra _ (FreeIsAlgebra v) +FreeAlgebra v = MkAlgebra + { U = Term sig v + , sem = \op => MkSetoidHomomorphism (Call op) (\_, _ => Call op) + } public export bindTermCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t} -- cgit v1.2.3