Adds a typevec simp attribute. Has to be in a separate file from TypeVec.lean, since simp attributes cannot be used directly in the file that declares them.

ink

def Parser.Attr.typevec : Lean.ParserDescr

simp set for the manipulation of typevec and arrow expressions

Equations

• One or more equations did not get rendered due to their size.