coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Why no unfolding on left in match?
- Date: Wed, 08 Oct 2014 17:37:31 -0400
On 10/08/2014 05:04 PM, Greg Morrisett wrote:
Yes. I just want some syntactic support to make this lighter weight. (Maybe
it can be done with clever notation now?). Bonus points if your solution
supports nested patterns.
The classic example is wanting to match a string based on regexps.
-Greg
Probably the correct answer is "write a DSL". The inductive view/total function/match idiom is so general purpose that a lighter weight syntax would probably limit its capabilities in some way. Unless you just mean by omitting redundant parts. For example, in this case, we currently have:
Inductive isFoo(i : nat) : Type :=
| Yes(eq : i = foo)
| No(neq : i <> foo).
Definition IsFoo(i : nat) : isFoo i :=
match (Nat.eq_dec i foo) with
| left e => Yes i e
| right e => No i e
end.
Maybe syntactic sugar-coat both of those definitions into one like so:
View IsFoo(i : nat) : Type :=
match (Nat.eq_dec i foo) with
| left e => Yes e
| right e => No e
end.
If you then combined this into the target match in the bar function, you'd actually be reducing abstraction - since the IsFoo view may be is useful to functions other than bar. You would then have to argue that Coq doesn't promote local definitions instead of that it doesn't promote abstraction.
-- Jonathan
- [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Adam Chlipala, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Enrico Tassi, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Abhishek Anand, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Adam Chlipala, 10/08/2014
Archive powered by MHonArc 2.6.18.