[Merged by Bors] - feat(data/matrix/notation): add !![1, 2; 3, 4] notation
#14991
Conversation
This means that a `vector` from a tactic block can be used in an expression.
…to eric-wieser/better-matrix-notation
…to eric-wieser/matrix-wip
…on' into eric-wieser/matrix-wip
eric-wieser
added
the
awaiting-review
| /-- Convert a vector of pexprs to the pexpr constructing that vector.-/ | ||
| meta def _root_.pi_fin.to_pexpr : Π {n}, (fin n → pexpr) → pexpr | ||
| | 0 v := ``(![]) | ||
| | (n + 1) v := ``(vec_cons %%(v 0) %%(_root_.pi_fin.to_pexpr $ vec_tail v)) |
There was a problem hiding this comment.
This might be appropriate as a has_to_pexpr instance, so that %%v has this meaning automatically. As of writing we only have the obvious pexpr, expr, and reflected instances of this typeclass; but in principle we could add instances for all "containers" that sends a container of pexprs to the pexpr that constructs that container
There was a problem hiding this comment.
I'm not comfortable enough with has_to_pexpr to say the instance would be unproblematic (recalling all the issues with universe polymorphism). So I'm happy to keep it as-is.
src/data/matrix/notation.lean
Outdated
| /-- A version of `sep_by` that allows trailing delimiters, but requires at least one item -/ | ||
| private meta def sep_by' {α : Type} : parser unit → parser α → parser (list α) | ||
| | s p := do | ||
| fst ← p, | ||
| some () ← optional s | pure [fst], | ||
| some rest ← optional (sep_by' s p) | pure [fst], | ||
| pure (fst :: rest) | ||
|
|
||
| /-- A version of `many` that requires at least one -/ | ||
| private meta def at_least_one {α : Type} (p : parser α) : parser (list α) := | ||
| list.cons <$> p <*> (many p) |
There was a problem hiding this comment.
I'd like to see these in a higher-up file, maybe tactic/core.lean.
| /-- Convert a vector of pexprs to the pexpr constructing that vector.-/ | ||
| meta def _root_.pi_fin.to_pexpr : Π {n}, (fin n → pexpr) → pexpr | ||
| | 0 v := ``(![]) | ||
| | (n + 1) v := ``(vec_cons %%(v 0) %%(_root_.pi_fin.to_pexpr $ vec_tail v)) |
There was a problem hiding this comment.
I'm not comfortable enough with has_to_pexpr to say the instance would be unproblematic (recalling all the issues with universe polymorphism). So I'm happy to keep it as-is.
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
|
bors merge |
github-actions
bot
added
the
ready-to-merge
This adds `!![1, 2; 3, 4]` as a matlab-like shorthand for `matrix.of ![![1, 2], ![3, 4]]`. This has special support for empty arrays, where `!![,,,]` is a matrix with 0 rows and 3 columns, and `![;;;]` is a matrix with 3 rows and zero columns.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
!![1, 2; 3, 4] notation!![1, 2; 3, 4] notation
This adds `!![1, 2; 3, 4]` as a matlab-like shorthand for `matrix.of ![![1, 2], ![3, 4]]`. This has special support for empty arrays, where `!![,,,]` is a matrix with 0 rows and 3 columns, and `![;;;]` is a matrix with 3 rows and zero columns.
This adds
!![1, 2; 3, 4]as a matlab-like shorthand formatrix.of ![![1, 2], ![3, 4]]. This has special support for empty arrays, where!![,,,]is a matrix with 0 rows and 3 columns, and![;;;]is a matrix with 3 rows and zero columns.Split from #14665.