theory WWellForm imports"../Common/WellForm" Expr begin
definition wwf_J_mdecl :: "J_prog → cname → J_mb mdecl → bool" where "wwf_J_mdecl P C ≡ λ(M,Ts,T,(pns,body)). length Ts = length pns ∧ distinct pns ∧ this ∉ set pns ∧ fv body ⊆ {this} ∪ set pns"
lemma wwf_J_mdecl[simp]: "wwf_J_mdecl P C (M,Ts,T,pns,body) = (length Ts = length pns ∧ distinct pns ∧ this ∉ set pns ∧ fv body ⊆ {this} ∪ set pns)" (*<*)by(simp add:wwf_J_mdecl_def)(*>*)
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 und die Messung sind noch experimentell.
