Nuprl - Some Definitions

Formula	`Def Formula == rec(formula.Var+formula+(formulaformula)+(formulaformula)+(formulaformula))` `Thm* Formula Type`
Var	`Def Var == Atom` `Thm* Var Type`
f_or	`Def pq == inr(inr(inr(inl( < p,q > ))))` `Thm* p,q:Formula. pq Formula`
fand	`Def pq == inr(inr(inl( < p,q > )))` `Thm* p,q:Formula. pq Formula`
fimp	`Def pq == inr(inr(inr(inr( < p,q > ))))` `Thm* p,q:Formula. pq Formula`
fnot	`Def p == inr(inl(p))` `Thm* x:Formula. x Formula`
formula_rank	`Def == (letrec formula_rank f = case f: x 0; p (formula_rank(p)+1); pq (formula_rank(p)+formula_rank(q)+1); pq (formula_rank(p)+formula_rank(q)+1); pq (formula_rank(p)+formula_rank(q)+1); )` `Thm* Formula`
fvar	`Def F == inl(F)` `Thm* x:Var. x Formula`
formula_case	`Def case F: x varC(x); p1 notC(p1); p2p3 andC(p2;p3); p4p5 orC(p4;p5); p6p7 impC(p6;p7); == InjCase(F; x. varC(x); F. InjCase(F; p1. notC(p1); F. InjCase(F; x. x/p2,p3.andC(p2;p3); F. InjCase(F; x. x/p4,p5.orC(p4;p5), x/p6,p7.impC(p6;p7)))))`
letrec_body	`Def = b == b`
letrec_arg	`Def x b(x) (x) == b(x)`
letrec	`Def (letrec f b(f)) == b((letrec f b(f)) ) (recursive)`

About: