Stream: Equations devs & users

Topic: Syntax of `with`


view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jason Gross (Nov 11 2022 at 15:25):

What's the magic that I lose by moving to a match?

view this post on Zulip 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?

view this post on Zulip 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…).

view this post on Zulip Paolo Giarrusso (Nov 11 2022 at 20:09):

Most importantly you'd lose Equations dependent pattern matching


Last updated: Jan 29 2023 at 16:02 UTC