Nuprl - Definition Cascade for assert

WhoCites Definitions hol arithmetic 3 Sections HOLlib Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
NOTE: This operator coercing a

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

Who Cites assert?

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

ifthenelse Def if b t else f fi == InjCase(b ; t; f)
Thm* b:, A:Type, p,q:A. if b p else q fi A

Syntax: b has structure: assert(b)

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions hol arithmetic 3 Sections HOLlib Doc

	Who Cites assert?

assert	Def b == if b True else False fi

	Thm* b:. b Prop

ifthenelse	Def if b t else f fi == InjCase(b ; t; f)

	Thm* b:, A:Type, p,q:A. if b p else q fi A