Nuprl Definition : int_term_to_rP
int_term_to_rP(t) ==
int_term_ind(t;
itermConstant(c)⇒ [1; c];
itermVar(v)⇒ [2; v];
itermAdd(l,r)⇒ rl,rr.eager-append(rl;eager-append(rr;[3]));
itermSubtract(l,r)⇒ rl,rr.eager-append(rl;eager-append(rr;[4]));
itermMultiply(l,r)⇒ rl,rr.eager-append(rl;eager-append(rr;[5]));
itermMinus(x)⇒ rx.eager-append(rx;[6]))
Definitions occuring in Statement :
int_term_ind: int_term_ind,
eager-append: eager-append(as;bs),
cons: [a / b],
nil: [],
natural_number: $n
Definitions occuring in definition :
int_term_ind: int_term_ind,
eager-append: eager-append(as;bs),
cons: [a / b],
natural_number: $n,
nil: []
FDL editor aliases :
int_term_to_rP
Latex:
int\_term\_to\_rP(t) ==
int\_term\_ind(t;
itermConstant(c){}\mRightarrow{} [1; c];
itermVar(v){}\mRightarrow{} [2; v];
itermAdd(l,r){}\mRightarrow{} rl,rr.eager-append(rl;eager-append(rr;[3]));
itermSubtract(l,r){}\mRightarrow{} rl,rr.eager-append(rl;eager-append(rr;[4]));
itermMultiply(l,r){}\mRightarrow{} rl,rr.eager-append(rl;eager-append(rr;[5]));
itermMinus(x){}\mRightarrow{} rx.eager-append(rx;[6]))
Date html generated:
2017_09_29-PM-05_54_39
Last ObjectModification:
2017_05_12-PM-11_29_28
Theory : omega
Home
Index