packages feed

descript-lang-0.2.0.0: test-resources/refactors/Macros.free-bind.dscr

//Macros

UZero[].
USucc[prev].
Sub[a, b].
Neg[a].

Nat[].
Untyped[].
Zero[].
Succ[prev].
Add[a, b].

//Macros
UZero[]: Zero[] | Untyped[]
USucc[prev]: Succ[prev: prev<USucc] | Untyped[]

Add[a, b]: Add[
  a: a<Add
  b: b<Add
]

---

Add[a: Nat[], b: Nat[]] | Untyped[]: Nat[]
Add[a: Zero[], b]: b<Add
Add[a: Succ[prev], b]: Add[a: a<Add>prev<Succ, b: Succ[prev: b<Add]]

UZero[]: Zero[] | Nat[]
USucc[prev: Nat[]]: Nat[]

Add[
  a: Succ[prev: Succ[prev: Succ[prev: Zero[] | Untyped[]] | Untyped[]] | Untyped[]] | Untyped[]
  b: Succ[prev: Succ[prev: Zero[] | Untyped[]] | Untyped[]] | Untyped[]
] | Untyped[]?