diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-07 12:32:59 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-07 12:32:59 +0000 |
| commit | 3107ee7777b0709997975e28d9ef2a46bca8ca47 (patch) | |
| tree | c7c5b9d559bee331c92c61b4b0fe24d7b823b776 /src/Soat/SecondOrder/Algebra.idr | |
| parent | d0bafca5249e694474d7c8108a949d64c64dcea5 (diff) | |
Lift index of varFunc.
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' : _) |