Commit 2023-01-17 19:22 9e505148

View on Github →

feat: port Data.Typevec (#891) mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3 porting notes: currently this is full of major issues. Help welcome

Estimated changes

added theorem TypeVec.Arrow.ext
added def TypeVec.Arrow.mp
added def TypeVec.Arrow
added def TypeVec.Curry
added def TypeVec.PredLast
added def TypeVec.RelLast
added def TypeVec.Subtype_
added def TypeVec.append1
added theorem TypeVec.appendFun_aux
added theorem TypeVec.appendFun_comp
added theorem TypeVec.appendFun_inj
added def TypeVec.comp
added theorem TypeVec.comp_assoc
added theorem TypeVec.comp_id
added theorem TypeVec.const_append1
added theorem TypeVec.const_iff_true
added theorem TypeVec.const_nil
added def TypeVec.diagSub
added theorem TypeVec.diag_sub_val
added def TypeVec.drop
added def TypeVec.dropFun
added theorem TypeVec.dropFun_comp
added theorem TypeVec.dropFun_diag
added theorem TypeVec.dropFun_id
added theorem TypeVec.dropFun_prod
added theorem TypeVec.drop_append1'
added theorem TypeVec.drop_append1
added theorem TypeVec.eq_nilFun
added theorem TypeVec.fst_diag
added theorem TypeVec.fst_prod_mk
added def TypeVec.id
added theorem TypeVec.id_comp
added theorem TypeVec.id_eq_nilFun
added def TypeVec.last
added def TypeVec.lastFun
added theorem TypeVec.lastFun_comp
added theorem TypeVec.lastFun_prod
added theorem TypeVec.last_append1
added def TypeVec.nilFun
added theorem TypeVec.nilFun_comp
added def TypeVec.ofRepeat
added def TypeVec.prod.fst
added def TypeVec.prod.mk
added def TypeVec.prod.snd
added def TypeVec.prod
added theorem TypeVec.prod_fst_mk
added theorem TypeVec.prod_id
added theorem TypeVec.prod_map_id
added theorem TypeVec.prod_snd_mk
added def TypeVec.relLast'
added def TypeVec.repeatEq
added theorem TypeVec.repeat_eq_nil
added theorem TypeVec.snd_diag
added theorem TypeVec.snd_prod_mk
added def TypeVec.splitFun
added theorem TypeVec.splitFun_comp
added theorem TypeVec.splitFun_inj
added theorem TypeVec.subtypeVal_nil
added def TypeVec