diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-06 13:50:12 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-06 13:50:12 +0000 |
| commit | 121965c3e550f285d3a428cbb6da10c97bfa9846 (patch) | |
| tree | fccec8224b7aae2fcf421e01b4440899ae45d22d /src/Soat/FirstOrder | |
| parent | df7df335a91878448a9f231c0af36f57874ccd4e (diff) | |
refactor: rename pwSetoid -> Product.
Diffstat (limited to 'src/Soat/FirstOrder')
| -rw-r--r-- | src/Soat/FirstOrder/Algebra/Coproduct.idr | 2 | ||||
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr index 88db184..548beed 100644 --- a/src/Soat/FirstOrder/Algebra/Coproduct.idr +++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr @@ -175,7 +175,7 @@ termToCoproduct x y = MkHomomorphism { func = MkIndexedSetoidHomomorphism (\_ => id) (\t, _, _ => tmRelImpliesCoprodRel) , semHomo = \op, tms => Call op $ - reflect (index (pwSetoid (CoproductAlgebra x y).setoid) _) $ + reflect (index (Product (CoproductAlgebra x y).setoid) _) $ sym $ mapId tms } diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index ee17093..2042d2f 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -159,7 +159,7 @@ bindHomo env = MkHomomorphism } , semHomo = \op, tms => a.algebra.semCong op $ - reflect (index (pwSetoid a.setoid) _) $ + reflect (index (Product a.setoid) _) $ bindTermsIsMap {a = a.raw} env.H tms } @@ -203,7 +203,7 @@ bindsUnique : {v : IndexedSetoid sig.T} -> {a : Algebra sig} -> (env : v ~> a.se -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func.H t (Done i)) (env.H t i)) -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) -> Pointwise a.relation (map f.func.H tms) (bindTerms {a = a.raw} env.H tms) -bindsUnique env f cong ts = CalcWith (index (pwSetoid a.setoid) _) $ +bindsUnique env f cong ts = CalcWith (index (Product a.setoid) _) $ |~ map f.func.H ts ~~ map (\_ => bindTerm {a = a.raw} env.H) ts ...( bindsUnique' f (bindHomo env) cong ts ) ~~ bindTerms {a = a.raw} env.H ts .=<( bindTermsIsMap {a = a.raw} env.H ts ) |