summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder/Algebra.idr
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2022-11-25 15:24:17 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2022-11-25 15:24:17 +0000
commit02f72834f36dbb3ff362f3876ebf87a2cebec0a8 (patch)
tree3ee8bd27d3eecfd497a9a8429ef5d64d1a4f90d0 /src/Soat/FirstOrder/Algebra.idr
parent1f867019430517435433ec55ad42dbf6770fd4fd (diff)
refactor: rename Homomorphism.f -> func.
Diffstat (limited to 'src/Soat/FirstOrder/Algebra.idr')
-rw-r--r--src/Soat/FirstOrder/Algebra.idr4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index bbc0430..5428ca3 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -60,5 +60,5 @@ public export
record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
where
constructor MkHomomorphism
- f : (t : sig.T) -> a.raw.U t -> b.raw.U t
- homo : IsHomomorphism a b f
+ func : IFunc a.raw.U b.raw.U
+ homo : IsHomomorphism a b func