diff options
Diffstat (limited to 'src/Soat/FirstOrder/Term.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 4 |
1 files changed, 2 insertions, 2 deletions
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 ) |