Nuprl Definition : test_case1
test_case1() == case TERMOF{decidable__q-constraints:o, 1:l} 1 [<λj.if j <z 2 then [1; 2][j] else 0 fi , 0>] of inl(y) \000C=> inl y | inr(x) => inr "not"
Definitions occuring in Statement :
select: L[n],
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x,
natural_number: $n,
token: "$token"
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
apply: f a,
pair: <a, b>,
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
select: L[n],
cons: [a / b],
natural_number: $n,
nil: [],
inl: inl x,
inr: inr x ,
token: "$token"
TermOfs occuring in Definition :
decidable__q-constraints
FDL editor aliases :
test_case1
Latex:
test\_case1() ==
case TERMOF\{decidable\_\_q-constraints:o, 1:l\} 1 [<\mlambda{}j.if j <z 2 then [1; 2][j] else 0 fi , 0>] of in\000Cl(y) => inl y | inr(x) => inr "not"
Date html generated:
2016_05_15-PM-11_33_24
Last ObjectModification:
2015_09_23-AM-08_30_03
Theory : rationals
Home
Index