Vincent Siles (Nov 13 2020 at 07:50): Vincent Siles (Nov 13 2020 at 07:50):Hi ! I have a function that returns a (nat * (A * B)) and atm I have to use let (n, foo) := ... in let (a, b) := foo in ... to get everything out. I kind of remember there was a way to write a more nested pattern, like let (n, (a, b)) := ... directly but can't find it again. Is is possible ? Am I mistaken ?
Théo Winterhalter (Nov 13 2020 at 07:53):Hi, you just add ' in front of the pattern.
Théo Winterhalter (Nov 13 2020 at 07:53):let '(a, (b,c)) := foo in ...
' , lovely thank you. I remembered something around : but not '. Is it in the doc ? I really tried to look it up but with no luck
Théo Zimmermann (Nov 13 2020 at 08:04):Yes, it's documented here: https://coq.github.io/doc/v8.12/refman/language/extensions/match.html#second-destructuring-let-syntax
Karl Palmskog (Nov 13 2020 at 08:18):are you using ssreflect? In this case let: will be the go-to choice: https://coq.github.io/doc/v8.12/refman/proof-engine/ssreflect-proof-language.html#pattern-assignment
Théo Zimmermann (Nov 13 2020 at 08:36):@Karl Palmskog: Do you have any concrete reason to recommend let: over let '? We were precisely discussing with @Enrico Tassi about getting rid (at least) of the implementation of let: and plug it to mean let ' or even about deprecating the syntax (this last part was less clear given the probably large number of use cases in existing code).
Théo Zimmermann (Nov 13 2020 at 08:38):BTW, note that the ' irrefutable pattern syntax can also be used directly in the binder syntax, e.g., when defining a function (https://coq.github.io/doc/v8.12/refman/language/core/assumptions.html#binders).
Vincent Siles (Nov 13 2020 at 08:39):Karl Palmskog said:
are you using ssreflect? In this case
let:will be the go-to choice: https://coq.github.io/doc/v8.12/refman/proof-engine/ssreflect-proof-language.html#pattern-assignment
So this is where my memory comes from :) I used to when I was in Chalmers, but I kind of forgot my way through ssr libs, so I'm using plain Coq atm
Karl Palmskog (Nov 13 2020 at 08:55):@Théo Zimmermann basically, if you are committing to using ssreflect, you use all its operators/idioms. If not, then not. There is indeed tons of code using let:, so getting rid of it would be a big endeavour
Karl Palmskog (Nov 13 2020 at 08:57):I don't really care how it's implemented under the hood as long as semantics and syntax is preserved
Théo Zimmermann (Nov 13 2020 at 08:58):Our point (and this was the plan since the SSR integration in Coq 8.7) is to make SSR a proof language and only that. So all of its extensions to the vernacular / to Gallina must be eventually merged into Coq. Syntax-wise, the merging might indeed require to keep the existing syntax ad vitam eternam if the compatibility impact of deprecating one of them would be too important.
Théo Zimmermann (Nov 13 2020 at 09:00):As another example, as you know, we are going to eventually remove the Search command that was provided by SSR but only once all SSR users are satisfied with the alternative we provide, and of course, it is easier to do with respect to compatibility since Search calls are rarely kept in finished proof scripts.
Last updated: Sep 23 2023 at 14:01 UTC