final?: false
eval: 'Nat[] | Succ[prev: Succ[prev: Succ[prev: Succ[prev: Succ[prev: Zero[]]]]]]'
refactor:
- label: singleton-record
  action: |
    reduce
    UZero[]
    Zero[] | Untyped[]
- label: singleton-record-new
  action: |
    reduce
    UZero[]
    UZeroq[]
- label: free-bind
  action: |
    reduce
    Neg[a: Sub[a: Neg[a], b: Neg[a]]]
    Add[a: a<Neg>a<Sub>a<Neg, b: a<Neg>b<Sub>a<Neg]
- label: parse-error
  action: |
    reduce
    Add[a: #Add[a, b]]
    Add[]
  error: |
    parse error: <interactive>:1:8:
      |
    1 | Add[a: #Add[a, b]]
      |        ^
    expected primitive type, got injected function application
- label: validation-error
  action: |
    reduce
    Add[a, b]
    Add[b: a<Add, b: b<Add]
  error: |-
    invalid:
    - line 1, columns 15 to 23: duplicate property: b: b<Add
- label: validation-error-ctx
  action: |
    reduce
    Add[a, b]
    Add[a: a<Add, b: b<Addq]
  error: |-
    invalid:
    - line 1, columns 20 to 24: nonexistent path: head not in input: Addq
- label: free-bind-complex-new
  action: |
    reduce
    Neg[a: Sub[a: Neg[a], b: Neg[a]]]
    Add3[a: a<Neg>a<Sub, b: a<Neg>b<Sub>a<Neg, c: Ignore[a: a<Neg>b<Sub>a<Neg]]