Commit 2023-01-23 16:46 392d4f4f

View on Github →

feat: port Data.Fin.VecNotation (#1741)

Estimated changes

added theorem Matrix.add_cons
added theorem Matrix.cons_add
added theorem Matrix.cons_add_cons
added theorem Matrix.cons_fin_one
added theorem Matrix.cons_head_tail
added theorem Matrix.cons_sub
added theorem Matrix.cons_sub_cons
added theorem Matrix.cons_val_one
added theorem Matrix.cons_val_succ'
added theorem Matrix.cons_val_succ
added theorem Matrix.cons_val_zero'
added theorem Matrix.cons_val_zero
added theorem Matrix.cons_vecAlt0
added theorem Matrix.cons_vecAlt1
added theorem Matrix.cons_vecAppend
added theorem Matrix.cons_zero_zero
added theorem Matrix.empty_add_empty
added theorem Matrix.empty_eq
added theorem Matrix.empty_sub_empty
added theorem Matrix.empty_val'
added theorem Matrix.empty_vecAlt0
added theorem Matrix.empty_vecAlt1
added theorem Matrix.empty_vecAppend
added theorem Matrix.head_add
added theorem Matrix.head_cons
added theorem Matrix.head_fin_const
added theorem Matrix.head_neg
added theorem Matrix.head_sub
added theorem Matrix.head_zero
added theorem Matrix.neg_cons
added theorem Matrix.neg_empty
added theorem Matrix.range_cons
added theorem Matrix.range_empty
added theorem Matrix.smul_cons
added theorem Matrix.smul_empty
added theorem Matrix.sub_cons
added theorem Matrix.tail_add
added theorem Matrix.tail_cons
added theorem Matrix.tail_neg
added theorem Matrix.tail_sub
added theorem Matrix.tail_zero
added def Matrix.vecAlt0
added def Matrix.vecAlt1
added def Matrix.vecAppend
added def Matrix.vecCons
added theorem Matrix.vecCons_const
added def Matrix.vecEmpty
added def Matrix.vecHead
added theorem Matrix.vecHead_vecAlt0
added theorem Matrix.vecHead_vecAlt1
added def Matrix.vecTail
added theorem Matrix.zero_empty