mirror of
https://github.com/unisonweb/unison.git
synced 2024-08-15 05:20:46 +03:00
0031542faf
This is for consistency with the `cmark` style. Now the blocks we still pretty-print ourselves will match the bulk of them that `cmark` produces.
1.1 KiB
1.1 KiB
Tests ability checking in scenarios where one side is concrete and the other is
a variable. This was supposed to be covered, but the method wasn't actually
symmetric, so doing equate l r might work, but not equate r l.
Below were cases that caused the failing order.
structural type W es = W
unique ability Zoot where
zoot : ()
woot : W {g} -> '{g, Zoot} a ->{Zoot} a
woot w a = todo ()
ex = do
w = (W : W {Zoot})
woot w do bug "why don't you typecheck?"
w1 : W {Zoot}
w1 = W
w2 : W {g} -> W {g}
w2 = cases W -> W
> w2 w1
Loading changes detected in scratch.u.
I found and typechecked these definitions in scratch.u. If you
do an `add` or `update`, here's how your codebase would
change:
⍟ These new definitions are ok to `add`:
structural type W es
ability Zoot
ex : '{Zoot} r
w1 : W {Zoot}
w2 : W {g} -> W {g}
woot : W {g} -> '{g, Zoot} a ->{Zoot} a
Now evaluating any watch expressions (lines starting with
`>`)... Ctrl+C cancels.
19 | > w2 w1
⧩
W