diff options
Diffstat (limited to 'src/Soat/SecondOrder/Algebra.idr')
| -rw-r--r-- | src/Soat/SecondOrder/Algebra.idr | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr index e52c945..038e065 100644 --- a/src/Soat/SecondOrder/Algebra.idr +++ b/src/Soat/SecondOrder/Algebra.idr @@ -155,8 +155,8 @@ public export } public export -(.varFunc) : (a : Algebra sig) -> (ctx : _) -> irrelevantCast (flip Elem ctx) ~> a.setoidAt ctx -(.varFunc) a ctx = mate (\_ => a.raw.var) +(.varFunc) : (a : Algebra sig) -> irrelevantCast (uncurry Elem) ~> a.setoid +(.varFunc) a = mate (\(_, _) => a.raw.var) public export (.substFunc) : (a : Algebra sig) -> (t : _) -> (ctx, ctx' : _) |