Nuprl Definition : int-palindrome-test
int-palindrome-test(L) ==
let x,y = fix((λlist_ind,L@0. eval v = L@0 in
if v is a pair then let x,xs' = v
in let a,ys = list_ind xs'
in let h,t = ys
in <case a
of inl() =>
if x=h then inl Ax else (inr Ax )
| inr() =>
inr Ax
, t
> otherwise if v = Ax then <inl Ax, L> otherwise ⊥))
L
in x
Definitions occuring in Statement :
bottom: ⊥,
callbyvalue: callbyvalue,
ispair: if z is a pair then a otherwise b,
isaxiom: if z = Ax then a otherwise b,
int_eq: if a=b then c else d,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x,
axiom: Ax
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
callbyvalue: callbyvalue,
ispair: if z is a pair then a otherwise b,
apply: f a,
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
int_eq: if a=b then c else d,
inr: inr x ,
isaxiom: if z = Ax then a otherwise b,
pair: <a, b>,
inl: inl x,
axiom: Ax,
bottom: ⊥
FDL editor aliases :
int-palindrome-test
Latex:
int-palindrome-test(L) ==
let x,y = fix((\mlambda{}list$_{ind}$,L@0. eval v = L@0 in
if v is a pair then let x,xs' = v
in let a,ys = list$_{ind}$ xs\000C'
in let h,t = ys
in <case a
of inl() =>
if x=h then inl Ax else (inr Ax )
| inr() =>
inr Ax
, t
> otherwise if v = Ax then <inl Ax, L> o\000Ctherwise \mbot{}))
L
in x
Date html generated:
2016_05_15-PM-07_37_23
Last ObjectModification:
2015_09_23-AM-08_17_29
Theory : general
Home
Index