diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:00:39 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:00:39 +0000 |
| commit | 580970d11a4e754c0c8e6f42c8312bffb1edc2db (patch) | |
| tree | 47e85bfd18a33ed6fd87e1c82181e5cdb5f6d43b /src/Soat/FirstOrder/Term.idr | |
| parent | 242197f40bb7957625be1e5f0bfd325af6e06be4 (diff) | |
Move IsAlgebra relation from type to body.
Diffstat (limited to 'src/Soat/FirstOrder/Term.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index eaa2da2..45282cc 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -130,12 +130,12 @@ Free : (0 V : sig.T -> Type) -> RawAlgebra sig Free v = MkRawAlgebra (Term sig v) Call public export -FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U) ((~=~) v.relation) -FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call' +FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U) +FreeIsAlgebra v = MkIsAlgebra ((~=~) v.relation) (tmRelEq v.equivalence) Call' public export FreeAlgebra : ISetoid sig.T -> Algebra sig -FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v) +FreeAlgebra v = MkAlgebra _ (FreeIsAlgebra v) public export bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v} |