Nuprl - Some Definitions

Thms list 3 autom Sections AutomataTheory Doc

NOTE: This operator coercing a

to a Prop is normally invisible since it is pretty obvious when it is needed.

assert Def b == if b True else False fi
Thm* b:. b Prop

iff Def P Q == (P Q) & (P Q)
Thm* A,B:Prop. (A B) Prop

lshort Def LShort(l) == Case of l; nil nil ; h.l' h.(LShort(l') \ h) (recursive)
Thm* St:Type, l:St*, eq:(StSt). LShort(l) St*

mem_f Def mem_f(T;a;bs) == Case of bs; nil False ; b.bs' b = a T mem_f(T;a;bs') (recursive)
Thm* T:Type, a:T, bs:T*. mem_f(T;a;bs) Prop

rev_implies Def P Q == Q P
Thm* A,B:Prop. (A B) Prop

lremove Def l \ a == Case of l; nil nil ; h.l' if eq(a,h) l' \ a else h.(l' \ a) fi (recursive)
Thm* St:Type, l:St*, s:St, eq:(StSt). (l \ s) St*

About:

assert	`Def b == if b True else False fi` `Thm* b:. b Prop`
iff	`Def P Q == (P Q) & (P Q)` `Thm* A,B:Prop. (A B) Prop`
lshort	`Def LShort(l) == Case of l; nil nil ; h.l' h.(LShort(l') \ h) (recursive)` `Thm* St:Type, l:St, eq:(StSt). LShort(l) St`
mem_f	`Def mem_f(T;a;bs) == Case of bs; nil False ; b.bs' b = a T mem_f(T;a;bs') (recursive)` `Thm* T:Type, a:T, bs:T*. mem_f(T;a;bs) Prop`
rev_implies	`Def P Q == Q P` `Thm* A,B:Prop. (A B) Prop`
lremove	`Def l \ a == Case of l; nil nil ; h.l' if eq(a,h) l' \ a else h.(l' \ a) fi (recursive)` `Thm* St:Type, l:St, s:St, eq:(StSt). (l \ s) St`