Nuprl Definition : deq
EqDecider(T) == {eq:T ⟶ T ⟶ 𝔹| ∀x,y:T. (x = y ∈ T ⇐⇒ ↑(eq x y))}
Definitions occuring in Statement :
assert: ↑b,
bool: 𝔹,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
bool: 𝔹,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
equal: s = t ∈ T,
assert: ↑b,
apply: f a
FDL editor aliases :
deq
Latex:
EqDecider(T) == \{eq:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbB{}| \mforall{}x,y:T. (x = y \mLeftarrow{}{}\mRightarrow{} \muparrow{}(eq x y))\}
Date html generated:
2016_05_14-AM-06_06_15
Last ObjectModification:
2015_09_22-PM-05_48_11
Theory : equality!deciders
Home
Index