feat: Vec delab #61
feat: Vec delab #61
Conversation
alexkeizer
left a comment
alexkeizer
left a comment
There was a problem hiding this comment.
Thanks, having an unexpander would be nice! I'm not sold on changing the separator to ; (especially as your PR mixes the two: a three-element list would be written !![ x; y, z ], which looks very wrong to me), could you revert those changes?
Also, try to write the PR description so that it makes sense without looking at the diff (it becomes part of the git history, after all).
For example:
This PR adds an unexpander for the vector literal
!![...]notation, to improve readability of goal statements.
That also helps clarify, for example, if you meant to change the separator, or what your reasoning is for that.
Qpf/Util/Vec.lean
Outdated
| | `(!![$t; ]) => `($t) | ||
| | `(!![$t; $x]) => `(Vec.append1 $t $x) | ||
| | `(!![$t; $xs,* , $x]) => `(Vec.append1 !![$t; $xs,*] $x) |
There was a problem hiding this comment.
Why do you mix semi-colons and commas here? Did you mean to change the syntax?
Qpf/Util/Vec.lean
Outdated
| @[app_unexpander Vec.nil] | ||
| def nil_uex : Lean.PrettyPrinter.Unexpander | ||
| | `($_p) => `(!![]) | ||
|
|
||
| @[app_unexpander Vec.append1] | ||
| def append1_uex : Lean.PrettyPrinter.Unexpander | ||
| | `($_p !![$x,*] $r) => `(!![$(x.push r),* ]) | ||
| | `($_p !![$t; $x,*] $r) => `(!![$t; $(x.push r),* ]) | ||
| | _ => throw () -- unhandled | ||
|
|
||
| /-- info: !![ℤ, ℕ, Prop] : Vec Type (Nat.succ 0).succ.succ -/ | ||
| #guard_msgs in | ||
| #check !![ℤ, ℕ, Prop] |
There was a problem hiding this comment.
Nice! Adding an unexpander for this syntax is a really good idea!
Note that standard Lean/Mathlib style does not indent after a section or namespace.
QPFTypes largely does not follow this style, but we probably should for new code so that eventually we are consistent.
That is, please remove the indentation here; but don't worry about the rest of the file (unless you feel particularly inspired to make a separate style cleanup PR)
|
Sorry the [x; a,b] means that you concat a and b onto x, three element lists still have the same syntax. I can revert this though I just added it so it would apply in more situations, so the type of x would be a Vec |
At first glance I'm not the biggest fan, as it looks misleadingly similar, why not write |
|
Sounds good! I realise that it meant to be a | as in Prolog for [x|a,b] |
alexkeizer
left a comment
alexkeizer
left a comment
There was a problem hiding this comment.
LGTM, feel free to merge after accepting the suggestion!
Thanks for the PR
Co-authored-by: Alex Keizer <alex@keizer.dev>
This PR adds an unexpander for the vector literal !![...] notation, to improve readability of goal statements.