Nuprl Definition : strict
strict(F) ==
(∀x:Base. ((F x)↓ ⇒ (x)↓))
∧ (∀u,v:Base. (F (exception(u; v)) ~ exception(u; v)))
∧ (∀z:Base. (is-exception(F z) ⇒ is-exception(z)))
Definitions occuring in Statement :
has-value: (a)↓,
is-exception: is-exception(t),
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
base: Base,
sqequal: s ~ t
Definitions occuring in definition :
has-value: (a)↓,
and: P ∧ Q,
sqequal: s ~ t,
all: ∀x:A. B[x],
base: Base,
implies: P ⇒ Q,
apply: f a,
is-exception: is-exception(t)
FDL editor aliases :
strict
Latex:
strict(F) ==
(\mforall{}x:Base. ((F x)\mdownarrow{} {}\mRightarrow{} (x)\mdownarrow{}))
\mwedge{} (\mforall{}u,v:Base. (F (exception(u; v)) \msim{} exception(u; v)))
\mwedge{} (\mforall{}z:Base. (is-exception(F z) {}\mRightarrow{} is-exception(z)))
Date html generated:
2016_05_13-PM-03_23_09
Last ObjectModification:
2015_09_22-PM-05_44_36
Theory : call!by!value_1
Home
Index