diff options
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} |