Definitions
array
1
Doc
At:
array
append
wf
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
k:
{j...}
5.
a:
[T]Array{i..j
}
6.
b:
[T]Array{j..k
}
a @ b
[T]Array{i..k
}
By:
OnMHyps [6;7;5;6] Analyze
Generated subgoal:
1
5.
a:
[T]Array
6.
a.l = i
7.
a.u = j
8.
b:
[T]Array
9.
b.l = j
10.
b.u = k
a @ b
[T]Array{i..k
}