coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Christian Doczkal <doczkal AT ps.uni-saarland.de>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Definition, Fixpoint, and simpl.
- Date: Wed, 9 Jul 2014 14:19:00 +0200
Hello Everyone
While refactoring a development I came across the following (at least for me)
surprising behavior:
Definition f (n:nat) := fix f m := match m with 0 => n | S m => f m end.
Fixpoint g (n m :nat) := match m with 0 => n | S m' => g n m' end.
Definition f3 := f 3.
Definition g3 := g 3.
Eval simpl in f3 3. (* = 3 *)
Eval simpl in g3 3. (* = g3 3 *)
I'm a little surprised that simpl unfolds f3 to expose and reduce the
fix/match but not g3 and I would be interested in knowing why this is the
case.
Thanks in advance for any replies.
--
Regards
Christian
- [Coq-Club] Definition, Fixpoint, and simpl., Christian Doczkal, 07/09/2014
- Re: [Coq-Club] Definition, Fixpoint, and simpl., Pierre Courtieu, 07/10/2014
Archive powered by MHonArc 2.6.18.