coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq rejects recursive call with obviously smaller principal argument

From: harke AT cs.pdx.edu
To: Eelis van der Weegen <coq-club AT contacts.eelis.net>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Coq rejects recursive call with obviously smaller principal argument
Date: Tue, 22 Apr 2008 12:23:23 -0700
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, Apr 22, 2008 at 09:00:17PM +0200, Eelis van der Weegen wrote:
]
] P.S. In the above, f is obviously a silly function. However, this is only an
] isolated testcase; in my actual development I'm trying to define a monadic
] bind operation for Tree.

How about:

Fixpoint bind' (A B:Set) (k:A -> Tree B) (m:Tree A) : Tree B :=
  match m with
  | Leaf a => k a
  | Node ts => Node _ (map (bind' _ _ k) ts)
  end.
Definition bind (A B:Set) m (k:A -> Tree B) := bind' A B k m.

--
Tom Harke
Portland State University

[Coq-Club] Coq rejects recursive call with obviously smaller principal argument, Eelis van der Weegen
- Re: [Coq-Club] Coq rejects recursive call with obviously smaller principal argument, harke
  - Re: [Coq-Club] Coq rejects recursive call with obviously smaller principal argument, Eelis van der Weegen