unison/unison-src/transcripts/records.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

3.9 KiB

Ensure that Records keep their syntax after being added to the codebase

Record with 1 field

unique type Record1 = { a : Text }
scratch/main> view Record1

  type Record1 = { a : Text }

Record with 2 fields

unique type Record2 = { a : Text, b : Int }
scratch/main> view Record2

  type Record2 = { a : Text, b : Int }

Record with 3 fields

unique type Record3 = { a : Text, b : Int, c : Nat }
scratch/main> view Record3

  type Record3 = { a : Text, b : Int, c : Nat }

Record with many fields

unique type Record4 =
  { a : Text
  , b : Int
  , c : Nat
  , d : Bytes
  , e : Text
  , f : Nat
  , g : [Nat]
  }
scratch/main> view Record4

  type Record4
    = { a : Text,
        b : Int,
        c : Nat,
        d : Bytes,
        e : Text,
        f : Nat,
        g : [Nat] }

Record with many many fields

unique type Record5 = {
  zero : Nat,
  one : [Nat],
  two : [[Nat]],
  three: [[[Nat]]],
  four: [[[[Nat]]]],
  five: [[[[[Nat]]]]],
  six: [[[[[[Nat]]]]]],
  seven: [[[[[[[Nat]]]]]]],
  eight: [[[[[[[[Nat]]]]]]]],
  nine: [[[[[[[[[Nat]]]]]]]]],
  ten: [[[[[[[[[[Nat]]]]]]]]]],
  eleven: [[[[[[[[[[[Nat]]]]]]]]]]],
  twelve: [[[[[[[[[[[[Nat]]]]]]]]]]]],
  thirteen: [[[[[[[[[[[[[Nat]]]]]]]]]]]]],
  fourteen: [[[[[[[[[[[[[[Nat]]]]]]]]]]]]]],
  fifteen: [[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]],
  sixteen: [[[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]]],
  seventeen: [[[[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]]]],
  eighteen: [[[[[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]]]]],
  nineteen: [[[[[[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]]]]]],
  twenty: [[[[[[[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]]]]]]]
}
scratch/main> view Record5

  type Record5
    = { zero : Nat,
        one : [Nat],
        two : [[Nat]],
        three : [[[Nat]]],
        four : [[[[Nat]]]],
        five : [[[[[Nat]]]]],
        six : [[[[[[Nat]]]]]],
        seven : [[[[[[[Nat]]]]]]],
        eight : [[[[[[[[Nat]]]]]]]],
        nine : [[[[[[[[[Nat]]]]]]]]],
        ten : [[[[[[[[[[Nat]]]]]]]]]],
        eleven : [[[[[[[[[[[Nat]]]]]]]]]]],
        twelve : [[[[[[[[[[[[Nat]]]]]]]]]]]],
        thirteen : [[[[[[[[[[[[[Nat]]]]]]]]]]]]],
        fourteen : [[[[[[[[[[[[[[Nat]]]]]]]]]]]]]],
        fifteen : [[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]],
        sixteen : [[[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]]],
        seventeen : [[[[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]]]],
        eighteen : [[[[[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]]]]],
        nineteen : [[[[[[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]]]]]],
        twenty : [[[[[[[[[[[[[[[[[[[[Nat]]]]]]]]]]]]]]]]]]]] }

Record with user-defined type fields

This record type has two fields whose types are user-defined (Record4 and UserType).

unique type UserType = UserType Nat

unique type RecordWithUserType = { a : Text, b : Record4, c : UserType }

If you view or edit it, it should be treated as a record type, but it does not (which is a bug)

scratch/main> view RecordWithUserType

  type RecordWithUserType
    = { a : Text, b : Record4, c : UserType }

Syntax

Trailing commas are allowed.

unique type Record5 =
  { a : Text,
    b : Int,
  }

  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`:
    
      Record5.a        : Record5 -> Text
      Record5.a.modify : (Text ->{g} Text)
                         -> Record5
                         ->{g} Record5
      Record5.a.set    : Text -> Record5 -> Record5
      Record5.b        : Record5 -> Int
      Record5.b.modify : (Int ->{g} Int)
                         -> Record5
                         ->{g} Record5
      Record5.b.set    : Int -> Record5 -> Record5
    
    ⍟ These names already exist. You can `update` them to your
      new definition:
    
      type Record5