From 841564f69f48a09b530853c3c075f269c7ebaf5b Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 2 Mar 2023 19:56:22 +0100 Subject: [PATCH] fix typo in comment --- lib/Quox/Syntax/Term/Base.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) ->