src/nat.bend checks
raw source on the hub · import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/nat.bend as MNat
2 imports
import Base import ./class.bend as C
Laws
law add_assoc provedsource · line 13 · raw
@a:Nat -> @b:Nat -> @c:Nat -> {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}plain binders, so it fits C.Semigroup's assoc field
law le_refl provedsource · line 41 · raw
@a:Nat -> LE(a, a)
law le_step provedsource · line 52 · raw
@a:Nat -> LE(a, 1n+a)
law le_trans provedsource · line 63 · raw
@a:Nat -> @b:Nat -> @c:Nat -> @ab:LE(a, b) -> @bc:LE(b, c) -> LE(a, c)
law sub_le provedsource · line 83 · raw
@a:Nat -> @k:Nat -> LE(Nat.sub(a, k), a)
a - k <= a (Nat.sub stops at 0)
law IsFalse provedsource · line 110 · raw
@c:Bool -> Type
Motives that refute {False{} == True{}} and {True{} == False{}}.
law IsTrue provedsource · line 121 · raw
@c:Bool -> Type
law le_of_is_lt provedsource · line 134 · raw
@a:Nat -> @b:Nat -> @e:{Nat.is_lt(a, b) == True{} : Bool} -> LE(a, b)The two outcomes of Nat.is_lt as LE proofs. Base's min, max and clamp branch on is_lt.
law ge_of_not_lt provedsource · line 150 · raw
@a:Nat -> @b:Nat -> @e:{Nat.is_lt(a, b) == False{} : Bool} -> LE(b, a)
Definitions
def LE source · line 28 · raw
@a:Nat -> @b:Nat -> Data
a <= b, as a type: Unit when it holds, Empty when it does not.
def LT source · line 38 · raw
@a:Nat -> @b:Nat -> Data
a < b. LT(i, 0n) computes to Empty.
def le_case source · line 100 · raw
@a:Nat -> @b:Nat -> Or(LE(a, b), LE(b, a))
Compares a and b and returns the proof of the side that holds.
def ord source · line 169 · raw
0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<Nat>
Nat ordered by LE
def add_sg source · line 173 · raw
0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Semigroup<Nat>
Nat under addition