Commit 2023-04-20 04:08 a06db5f8

View on Github →

feat: port Data.Matrix.Notation (#3427) This PR also fixes the doc on Data.Fin.VecNotation and adds the unexpander for the ![x, y, ...] notation.

Estimated changes

added theorem Matrix.col_cons
added theorem Matrix.col_empty
added theorem Matrix.cons_dotProduct
added theorem Matrix.cons_mul
added theorem Matrix.cons_mulVec
added theorem Matrix.cons_transpose
added theorem Matrix.cons_val'
added theorem Matrix.cons_vecMul
added theorem Matrix.cons_vecMulVec
added theorem Matrix.dotProduct_cons
added theorem Matrix.empty_mul
added theorem Matrix.empty_mulVec
added theorem Matrix.empty_mul_empty
added theorem Matrix.empty_vecMul
added theorem Matrix.empty_vecMulVec
added theorem Matrix.eta_fin_three
added theorem Matrix.eta_fin_two
added theorem Matrix.head_transpose
added theorem Matrix.head_val'
added theorem Matrix.mulVec_cons
added theorem Matrix.mulVec_empty
added theorem Matrix.mul_empty
added theorem Matrix.mul_fin_three
added theorem Matrix.mul_fin_two
added theorem Matrix.mul_val_succ
added theorem Matrix.one_fin_three
added theorem Matrix.one_fin_two
added theorem Matrix.row_cons
added theorem Matrix.row_empty
added theorem Matrix.smul_mat_cons
added theorem Matrix.smul_mat_empty
added theorem Matrix.smul_vec2
added theorem Matrix.smul_vec3
added theorem Matrix.submatrix_empty
added theorem Matrix.tail_transpose
added theorem Matrix.tail_val'
added theorem Matrix.vec2_add
added theorem Matrix.vec2_dotProduct
added theorem Matrix.vec2_eq
added theorem Matrix.vec3_add
added theorem Matrix.vec3_dotProduct
added theorem Matrix.vec3_eq
added theorem Matrix.vecMulVec_cons
added theorem Matrix.vecMulVec_empty
added theorem Matrix.vecMul_cons
added theorem Matrix.vecMul_empty
added def Matrix.mkMatrix