(2steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
seq
cons
wf
A
:Type,
n
:
,
x
:
A
,
xs
:(
(
n
-1)
A
). [
x
/
xs
]
n
A
By:
Def of [
x
/
xs
] THEN Guarding if <bool>
<*> else <else> fi Auto
Generated subgoal:
1
1.
A
: Type
2.
n
:
3.
x
:
A
4.
xs
:
(
n
-1)
A
5.
i
:
n
if
i
=
0
x
else
xs
(
i
-1) fi
A
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A:Type, n:
, x:A, xs:((n-1)
A). [x/ xs] 
nA A:Type, n:, x:A, xs:((n-1)A). [x/ xs] nA
<*> else <else> fi Auto
(n-1)A
n
if i=
0 x else xs(i-1) fi A
