data LNat : Type
Linear Nat
0 toNat : LNat -@ Nat
Convert a linear nat to an unrestricted Nat, only usable at the type level
because we canot call `S` with an argument that is expected to be used exactly once
add : LNat -@ (LNat -@ LNat)
Add two linear numbers
mult : (1 n : LNat) -> (0 l : LNat) -> {auto 1 _ : toNat n `Copies` l} -> LNat
Multiply two linear numbers
square : (1 v : LNat) -> {auto 1 _ : toNat v `Copies` v} -> LNat
Square a linear number