Def b == if b True else False fi

is mentioned by

Thm* A:Type, eq:EqDecider(A), f:a:A fp-> Top. Thm* fpf-dom-list(f)  {a:A| a  dom(f) } List	[fpf-dom-list_wf]
Thm* eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v)  x = y	[fpf-single-dom]
Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A. Thm* x  dom(f  g)  x  dom(f)  x  dom(g)	[fpf-join-dom2]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x  dom(f  g)  x  dom(f)  x  dom(g)	[fpf-join-dom]
Def ma-sframe-compatible(A; B) Def == kl:(KndIdLnk), tg:Id. Def == (kl  dom(1of(2of(2of(2of(2of(2of(A))))))) Def == ( Def == ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(A))))))(kl))) Def == ( Def == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A))))))))) Def == ( Def == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B))))))))) Def == ( Def == (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of( Def == (deq-member(KindDeq;1of(kl);1of(B))))))))(<2of(kl),tg>))) Def == & (kl  dom(1of(2of(2of(2of(2of(2of(B))))))) Def == & ( Def == & ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(B))))))(kl))) Def == & ( Def == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B))))))))) Def == & ( Def == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A))))))))) Def == & ( Def == & (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of( Def == & (deq-member(KindDeq;1of(kl);1of(A))))))))(<2of(kl),tg>)))	[ma-sframe-compatible]
Def ma-frame-compatible(A; B) Def == kx:(KndId).  Def == (kx  dom(1of(2of(2of(2of(2of(A)))))) Def == ( Def == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A)))))))) Def == ( Def == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B)))))))) Def == ( Def == (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of( Def == (deq-member(KindDeq;1of(kx);1of(B)))))))(2of(kx)))) Def == & (kx  dom(1of(2of(2of(2of(2of(B)))))) Def == & ( Def == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B)))))))) Def == & ( Def == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A)))))))) Def == & ( Def == & (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of( Def == & (deq-member(KindDeq;1of(kx);1of(A)))))))(2of(kx))))	[ma-frame-compatible]
Def M.sframe(k sends <l,tg>) Def == L != 1of(2of(2of(2of(2of(2of(2of(2of( Def == L != 1of(M))))))))(<l,tg>) ==> deq-member(KindDeq;k;L)	[ma-sframe]
Def M.frame(k affects x) Def == L != 1of(2of(2of(2of(2of(2of(2of(M)))))))(x) ==> deq-member(KindDeq;k;L)	[ma-frame]
Def a declared in M == locl(a)  dom(1of(2of(M)))	[ma-decla]
Def xdom(f). v=f(x)   P(x;v) == x:A. x  dom(f)  P(x;f(x))	[fpf-all]
Def f || g == x:A. x  dom(f) & x  dom(g)  f(x) = g(x)  B(x)	[fpf-compatible]

In prior sections: bool 1 list 1 mb nat mb list 1 union mb list 2 mb event system 1 mb event system 2 mb event system 3 rel 1

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html