WhoCites
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites sfa
doc
sexpr
cases?
sfa_doc_sexpr_cases
Def Case of
s
: Inj(
x
)
g
(
x
) ; Cons(
s1
;
s2
)
f
(
s1
;
s2
)
Def
== InjCase(
s
;
s1s2
.
s1s2
/
s1
,
s2
.
f
(
s1
;
s2
);
x
.
g
(
x
))
Thm*
A
:Type,
C
:(Sexpr(
A
)
Type),
s
:Sexpr(
A
),
Thm*
f
:(
s1
,
s2
:Sexpr(
A
)
C
(Cons(
s1
;
s2
))),
g
:(
x
:
A
C
(Inj(
x
))).
Thm*
(Case of
s
: Inj(
x
)
g
(
x
) ; Cons(
s1
;
s2
)
f
(
s1
,
s2
))
C
(
s
)
Syntax:
Case of
s
: Inj(
x
)
g
(
x
) ; Cons(
s1
;
s2
)
f
(
s1
;
s2
)
has structure:
sfa_doc_sexpr_cases(
s
;
s1
,
s2
.
f
(
s1
;
s2
);
x
.
g
(
x
))
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc