~/bend-docscommunity

proofs/math/typed/f64sqw.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqw.bend as F64sqw

4 imports
import Base
import ../../../spec/math/f64.bend as SF
import ./natcmp.bend as NC
import ./f64cmp.bend as FC

Definitions

def ltz source · line 8 · raw

@+l:Nat -> {Nat.is_lt(0n, l) == Bool.not(Nat.is_eq(l, 0n)) : Bool}

def eq_comm source · line 15 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}

def and_comm source · line 18 · raw

@+a:Bool -> @+b:Bool -> {Bool.and(a, b) == Bool.and(b, a) : Bool}