descript-lang-0.2.0.0: test-resources/examples/Macros.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[]

Neg[a: Sub[a: Neg[a], b: Neg[a]]]: Add[
  a: a<Neg>a<Sub>a<Neg
  b: a<Neg>b<Sub>a<Neg
]

---

Add[a: Nat[], b: Nat[]] | Untyped[]: Nat[]
Neg[a: Sub[a: Neg[a: Zero[]], b: Neg[a]]]: a<Neg>b<Sub>a<Neg
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[]?