Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Definition, Fixpoint, and simpl.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Definition, Fixpoint, and simpl.


Chronological Thread 
  • 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


Archive powered by MHonArc 2.6.18.

Top of Page