Nuprl Definition : Form_size
Form_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "Var" then 0
if lbl =a "Const" then 0
if lbl =a "Set" then 1 + (size (snd(x)))
if lbl =a "Equal" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Member" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "And" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Or" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Not" then 1 + (size x)
if lbl =a "All" then 1 + (size (snd(x)))
if lbl =a "Exists" then 1 + (size (snd(x)))
else 0
fi ))
p
Definitions occuring in Statement :
ifthenelse: if b then t else f fi
,
eq_atom: x =a y
,
pi1: fst(t)
,
pi2: snd(t)
,
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]
,
spread: spread def,
pi1: fst(t)
,
ifthenelse: if b then t else f fi
,
eq_atom: x =a y
,
token: "$token"
,
add: n + m
,
apply: f a
,
pi2: snd(t)
,
natural_number: $n
FDL editor aliases :
Form_size
Form_size
Latex:
Form\_size(p) ==
fix((\mlambda{}size,p. let lbl,x = p
in if lbl =a "Var" then 0
if lbl =a "Const" then 0
if lbl =a "Set" then 1 + (size (snd(x)))
if lbl =a "Equal" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Member" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "And" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Or" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Not" then 1 + (size x)
if lbl =a "All" then 1 + (size (snd(x)))
if lbl =a "Exists" then 1 + (size (snd(x)))
else 0
fi ))
p
Date html generated:
2018_05_21-PM-10_42_11
Last ObjectModification:
2017_10_10-PM-04_31_31
Theory : PZF
Home
Index