Idris2Doc : Data.Linear.LNat

Data.Linear.LNat

Definitions

dataLNat : Type
  Linear Nat

Totality: total
Visibility: public export
Constructors:
Zero : LNat
Succ : LNat-@LNat

Hints:
ConsumableLNat
DuplicableLNat
0toNat : 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

Totality: total
Visibility: public export
add : LNat-@ (LNat-@LNat)
  Add two linear numbers

Totality: total
Visibility: export
mult : (1n : LNat) -> (0l : LNat) -> {auto1_ : toNatn `Copies` l} ->LNat
  Multiply two linear numbers

Totality: total
Visibility: export
square : (1v : LNat) -> {auto1_ : toNatv `Copies` v} ->LNat
  Square a linear number

Totality: total
Visibility: export