Data.Linear.LNat

Definitions

data LNat : Type

  Linear Nat

Totality: total
Visibility: public export
Constructors:

Zero : LNat

Succ : LNat -@ LNat

Hints:

Consumable LNat

Duplicable LNat

0 toNat : LNat -@ Nat

  Convert a linear nat to an unrestricted Nat, only usable at the type level
  because we cannot call `S` with an argument that is expected to be used exactly once

Totality: total
Visibility: public export

add : LNat -@ (LNat -@ LNat)

  Add two linear numbers

Totality: total
Visibility: export

mult : (1 n : LNat) -> (0 l : LNat) -> {auto 1 _ : toNat n `Copies` l} -> LNat

  Multiply two linear numbers

Totality: total
Visibility: export

square : (1 v : LNat) -> {auto 1 _ : toNat v `Copies` v} -> LNat

  Square a linear number

Totality: total
Visibility: export