diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr index 4e50f88..b923d4c 100644 --- a/lib/Quox/Syntax/Term/Base.idr +++ b/lib/Quox/Syntax/Term/Base.idr @@ -96,7 +96,7 @@ mutual ||| pair destruction ||| ||| `CasePair ๐œ‹ ๐‘’ ([๐‘Ÿ], ๐ด) ([๐‘ฅ, ๐‘ฆ], ๐‘ก)` is - ||| `๐œ๐š๐ฌ๐ž ๐œ‹ ยท ๐‘’ ๐ซ๐ž๐ญ๐ฎ๐ซ๐ง ๐‘Ÿ โ‡’ ๐ด ๐จ๐Ÿ { (๐‘ฅ, ๐‘ฆ) โ‡’ ๐‘ก }` + ||| `๐œ๐š๐ฌ๐ž ๐œ‹ ยท ๐‘’ ๐ซ๐ž๐ญ๐ฎ๐ซ๐ง ๐‘Ÿ โ‡’ ๐ด ๐จ๐Ÿ { (๐‘ฅ, ๐‘ฆ). ๐‘ก }` CasePair : (qty : q) -> (pair : Elim q d n) -> (ret : ScopeTerm q d n) -> (body : ScopeTermN 2 q d n) ->