|
(* Title: HOL/HOLCF/ex/Letrec.thy
Author: Brian Huffman
*)
section \<open>Recursive let bindings\<close>
theory Letrec
imports HOLCF
begin
definition
CLetrec :: "('a::pcpo \ 'a \ 'b::pcpo) \ 'b" where
"CLetrec = (\ F. snd (F\(\ x. fst (F\x))))"
nonterminal recbinds and recbindt and recbind
syntax
"_recbind" :: "[logic, logic] \ recbind" ("(2_ =/ _)" 10)
"" :: "recbind \ recbindt" ("_")
"_recbindt" :: "[recbind, recbindt] \ recbindt" ("_,/ _")
"" :: "recbindt \ recbinds" ("_")
"_recbinds" :: "[recbindt, recbinds] \ recbinds" ("_;/ _")
"_Letrec" :: "[recbinds, logic] \ logic" ("(Letrec (_)/ in (_))" 10)
translations
(recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
(recbindt) "x = a, y = b" == (recbindt) "(x,y) = (a,b)"
translations
"_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)"
"Letrec xs = a in (e,es)" == "CONST CLetrec\(\ xs. (a,e,es))"
"Letrec xs = a in e" == "CONST CLetrec\(\ xs. (a,e))"
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
