Jason Gross (Nov 09 2022 at 17:03): Jason Gross (Nov 09 2022 at 17:03):MetaCoq has a bunch of things like
| @exist (Some (args, c, ρ)) eq2 with inspect (reduce c (Fix_app mfix idx args :: ρ) _) := {
| @exist (@exist (t, ρ') prf) eq3 with construct_viewc t := {
where there are sequencted with clauses.
Is there a way to get a monadic variant of with to work syntactically, where monadic_with foo := { clauses } desugars to bind foo (fun v => with v := { clauses })? (What even is the syntax to get with foo := { clauses } when you're in the middle of a program rather than at a branch?)
into something that does a monadic bind on reduce either before or after the inspect?
| @exist (Some (args, c, ρ)) eq2 :=
'(@exist (t, ρ') prf) <- reduce c (Fix_app mfix idx args :: ρ) _;;
with construct_viewc t := {
is a syntax error...
Théo Winterhalter (Nov 10 2022 at 08:37):A with in the middle would just be a match but then you can't hope for Equations to operate its magic.
James Wood (Nov 10 2022 at 09:49):I guess the dual solution is to use a where definition, where you have to repeat your type signature, but you get to carry on using Equations' mechanisms.
Jason Gross (Nov 11 2022 at 15:25):What's the magic that I lose by moving to a match?
Jason Gross (Nov 11 2022 at 15:26):And is there a way to write a where clause that keeps the code near this branch, or does the where have to move to top-level?
Théo Winterhalter (Nov 11 2022 at 15:35):Jason Gross said:
What's the magic that I lose by moving to a
match?
I think all that goes into generating the term as well as the various associated principles (such as the graph, functional elimination…).
Paolo Giarrusso (Nov 11 2022 at 20:09):Most importantly you'd lose Equations dependent pattern matching
Last updated: Sep 15 2024 at 12:01 UTC