mlib_linalg.bend checks
raw source on the hub · import 0x4c3090ea8722081700f9d99ea7503e43/mlib_linalg.bend as Mlib_linalg
1 import
import Base
Laws
law mmat_add_1234_5678 provedsource · line 87 · raw
{mmat_add(mmat_mk(1n, 2n, 3n, 4n), mmat_mk(5n, 6n, 7n, 8n)) == mmat_mk(6n, 8n, 10n, 12n) : Mat2}
law mmat_mul_12_34 provedsource · line 94 · raw
{mmat_mul(mmat_mk(1n, 2n, 3n, 4n), mmat_mk(5n, 6n, 7n, 8n)) == mmat_mk(19n, 22n, 43n, 50n) : Mat2}
law mmat_det_example provedsource · line 101 · raw
{mmat_det(mmat_example) == 10n : Nat}
law mmat_trace_example provedsource · line 107 · raw
{mmat_trace(mmat_example) == 7n : Nat}
law mmat_id_mul provedsource · line 113 · raw
{mmat_mul(mmat_id, mmat_example) == mmat_example : Mat2}
law mmat_add_zero provedsource · line 119 · raw
{mmat_add(mmat_example, mmat_zero) == mmat_example : Mat2}
law mmat_eq_refl provedsource · line 125 · raw
{mmat_eq(mmat_example, mmat_example) == True{} : Bool}
Types
type Mat2 source · line 15 · raw
Data
MMat@a:Nat -> @b:Nat -> @c:Nat -> @d:Nat -> Mat2
Definitions
def mmat_mk source · line 20 · raw
@a:Nat -> @b:Nat -> @c:Nat -> @d:Nat -> Mat2
def mmat_zero source · line 23 · raw
Mat2
def mmat_id source · line 26 · raw
Mat2
def mmat_example source · line 29 · raw
Mat2
def mmat_a source · line 34 · raw
@m:Mat2 -> Nat
def mmat_b source · line 39 · raw
@m:Mat2 -> Nat
def mmat_c source · line 44 · raw
@m:Mat2 -> Nat
def mmat_d source · line 49 · raw
@m:Mat2 -> Nat
def mmat_add source · line 56 · raw
@a:Mat2 -> @b:Mat2 -> Mat2
def mmat_mul source · line 61 · raw
@+a:Mat2 -> @+b:Mat2 -> Mat2
def mmat_det source · line 69 · raw
@m:Mat2 -> Nat
def mmat_trace source · line 74 · raw
@m:Mat2 -> Nat
def mmat_eq source · line 79 · raw
@a:Mat2 -> @b:Mat2 -> Bool