The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Why should this be a problem?  I do not know of any programming
language with a pattern matching facility which would disallow this.

On 03.04.2014 18:13, Christian Doczkal wrote:
> Hello
> 
> I was surprised to find out that the following does not generate
> any errors:
> 
> Goal forall (X Y : Type) (s : X) (p : X -> Y), (let x := s in p x)
> = (match s with x => p x end). reflexivity.
> 
> Printing reveals, that the match above is probably eliminated
> before type checking. Nevertheless I find it strange that this
> input syntax is allowed.
> 
> Is this a bug or a feature? I suspect it has something to do with
> the match compilation.
> 


- -- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel AT gu.se
http://www2.tcs.ifi.lmu.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iEYEARECAAYFAlM+Un0ACgkQPMHaDxpUpLOH+QCeO/dDTSKotMRb5b4fYbh09knU
LDsAoI8rgTeY9WPI9Gmb3hpdumCLyHue
=EFFW
-----END PGP SIGNATURE-----