coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] Writing a recursive function that's not quite structurally recursive?
Chronological Thread
- From: Erik Silkensen <eriksilkensen AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Writing a recursive function that's not quite structurally recursive?
- Date: Sat, 2 Nov 2013 02:15:11 -0400
Hi all,
I was wondering if there’s a way to write a function like
Fixpoint f n :=
match n with
| 0 => True
| S m =>
forall m', m' <= m -> f m'
end.
where the recursive call is with a smaller argument, but it doesn’t come
directly from a constructor, if that makes sense?
You can tell I’m very new to Coq! I was just reading Adam Chlipala’s page on
well-founded recursion (http://adam.chlipala.net/cpdt/html/GeneralRec.html),
and am looking forward to studying it further, but was feeling a bit
overwhelmed at first, and thought I’d ask here in case there’s an easy way
around this example.
Thanks for any help.
-Erik
- [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Chris Dams, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, AUGER Cédric, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Chris Dams, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Rui Baptista, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, AUGER Cédric, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Adam Chlipala, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Chris Dams, 11/02/2013
Archive powered by MHonArc 2.6.18.