unisonweb/unison
1
0
Fork 0
mirror of https://github.com/unisonweb/unison.git synced 2024-08-15 13:30:27 +03:00
Code Issues Projects Releases Wiki Activity
trunk
unison/unison-src/transcripts/fix2423.output.md
Greg Pfeil 0031542faf
Add a space before code block info strings 
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.
2024-07-10 13:56:07 -06:00

1.2 KiB
Raw Permalink Blame History 

structural ability Split where
  skip! : x
  both : a -> a -> a

Split.append : '{Split, g} a -> '{Split, g} a -> '{Split, g} a 
Split.append s1 s2 _ = force (both s1 s2)

force a = !a

Split.zipSame : '{Split, g} a -> '{Split, g} b -> '{Split, g} (a, b)
Split.zipSame sa sb _ = 
  go : '{Split,g2} y -> Request {Split} x ->{Split,g2} (x,y)
  go sb = cases
    { a } -> (a, !sb)
    { skip! -> _ } -> skip!
    { both la ra -> k } -> 
      handle !sb with cases
        { _ } -> skip!
        { skip! -> k } -> skip!
        { both lb rb -> k2 } -> 
          force (Split.append
            (zipSame '(k la) '(k2 lb))
             (zipSame '(k ra) '(k2 rb)))

  handle !sa with go sb


  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 ability Split
      Split.append  : '{g, Split} a
                      -> '{g, Split} a
                      -> '{g, Split} a
      Split.zipSame : '{g, Split} a
                      -> '{g, Split} b
                      -> '{g, Split} (a, b)
      force         : '{g} o ->{g} o