Re: [isabelle] Some Remarks to Code Generation
Here is a small example:
theory Scratch imports Main
fun fib :: "nat \<Rightarrow> nat" where
"fib 0 = 0"
| "fib (Suc 0) = Suc 0"
| "fib (Suc (Suc n)) = fib (Suc n) + fib n"
value "map (fib o nat) [0..10]"
theorem fib_loop [code]:
"fib n = fib n"
export_code fib in Scala file "Fib.scala"
On 31.07.2012, at 18:38, Yannick Duchêne (Hibou57) wrote:
> Le Tue, 31 Jul 2012 18:13:12 +0200, Patrick Michel <uni at pbmichel.de> a écrit:
>> As it turns out it is quite easy to prove a code equation that obviously leads to non-terminating execution.
> I've not reached that point (still learning Isabelle and HOL), but I'm already interested in this, as I will generate SML programs from proofs. Can you please, provide a concrete example of an erroneous proof of a non‑terminating function?
> “Syntactic sugar causes cancer of the semi-colons.” 
> “Structured Programming supports the law of the excluded muddle.” 
> : Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and