Definitions
array
1
Doc
At:
array
shift
wf
T:Type, i:
, j:{i...}, a:[T]Array{i..j
}, m:
. a[++m]
[T]Array{i+m..j+m
}
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
a:
[T]Array{i..j
}
5.
m:
a[++m]
[T]Array{i+m..j+m
}