Nuprl Definition : formulaco_size
formulaco_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "var" then 0
if lbl =a "not" then 1 + (size x)
if lbl =a "and" then let left,right = x in (1 + (size left)) + (size right)
if lbl =a "or" then let left,right = x in (1 + (size left)) + (size right)
if lbl =a "imp" then let left,right = x in (1 + (size left)) + (size right)
else 0
fi ))
p
Definitions occuring in Statement :
ifthenelse: if b then t else f fi
,
eq_atom: x =a y
,
apply: f a
,
fix: fix(F)
,
lambda: λx.A[x]
,
spread: spread def,
add: n + m
,
natural_number: $n
,
token: "$token"
Definitions occuring in definition :
fix: fix(F)
,
lambda: λx.A[x]
,
ifthenelse: if b then t else f fi
,
eq_atom: x =a y
,
token: "$token"
,
spread: spread def,
add: n + m
,
apply: f a
,
natural_number: $n
FDL editor aliases :
formulaco_size
Latex:
formulaco\_size(p) ==
fix((\mlambda{}size,p. let lbl,x = p
in if lbl =a "var" then 0
if lbl =a "not" then 1 + (size x)
if lbl =a "and" then let left,right = x in (1 + (size left)) + (size right)
if lbl =a "or" then let left,right = x in (1 + (size left)) + (size right)
if lbl =a "imp" then let left,right = x in (1 + (size left)) + (size right)
else 0
fi ))
p
Date html generated:
2016_05_15-PM-07_01_23
Last ObjectModification:
2015_09_23-AM-08_08_52
Theory : general
Home
Index