Commit 2025-04-17 23:56 dad08fa3

feat: PiFin.mkLiteralQ and Matrix.mkLiteralQ (#24101) This defines some new functions to match the Qq.mkSetLiteralQ from #23025. The commented pexpr function is really just the syntax quotation `(![$xs,*]), so it is no longer worth keeping around. This deliberately uses Fin n → Q($α) instead of Vector Q($α) n as the former saves needing to allocate an auxiliary array, and the latter still can be used by passing in v.get : Fin n → Q($α). This also cleans up and adds some related tests.