Re: [isabelle] New AFP entry: Mutually Recursive Partial Functions



Le Wed, 19 Feb 2014 09:57:24 +0100, Tobias Nipkow <nipkow at in.tum.de> a écrit:

Mutually Recursive Partial Functions
René Thiemann

We provide a wrapper around the partial-function command that supports mutual
recursion.

http://afp.sourceforge.net/entries/Partial_Function_MR.shtml

Enjoy!

Excuse my ignorance on a topic, I never cared before.

This entry is marked “License: BSD License” on the main page, and is marked “License: LGPL” on these pages:

* http://afp.sourceforge.net/browser_info/current/AFP/Partial_Function_MR/Partial_Function_MR.html * http://afp.sourceforge.net/browser_info/current/AFP/Partial_Function_MR/Partial_Function_MR_Examples.html

As far as I know (I may be wrong), BSD inside (L)GPL is OK, but not the other way.

Also by the way, another question I've never ask: in which way the license of a theory impacts what's proved after that theory? One may have the same question with program generation.


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.