[Agda] --no-pattern-matching

[Guillaume Brunerie]

Disallowing any kind of pattern matching is really extreme. As far as
I’m concerned, I would be happy with an option limiting pattern
matching to primitive recursion and where you can only match on one
variable at the same time (so that any use of pattern matching would
be equivalent to a single use of the corresponding eliminator).

Guillaume

2014/1/18 Andreas Abel <andreas.abel at ifi.lmu.de>:
> --no-pattern-matching is an extreme form of chastity, but it should not hard
> to implement it.  If I understood correctly, you want Agda to slap your
> fingers if you wrote a constructor pattern anywhere.
>
> The most principled way to implement this I can think of is to disallow any
> kind of splitting in the checking of function left hand sides.
>
> Cheers,
> Andreas
>
> On 17.01.2014 15:28, Matteo Acerbi wrote:
>>
>> every now and then I would like to forbid
>> myself to use pattern matching at all, at least from inside a single
>> file.
>>
>> I would like to have the possibility to get back to that file and make
>> sure that I never used pattern matching in that code just by looking
>> at the OPTIONS header.
>>
>> I think I would find a --no-pattern-matching option, which simply
>> applied this restriction, but still allowed for importing modules
>> whatever their options are, very convenient.
>>
>> For now I am just curious as to whether others are interested: would
>> anyone else like such a --no-pattern-matching option?
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda