Say that we have a value v of type [a,b:int] T(a, b).
The following line of code introduces two fresh static variables
a and b and then assigns the the type T(a, b) to x
val [a:int,b:int] x = v
Of course, x can be replaced with a pattern of another form.
The following dataprop is defined in prelude/basics_dyn.sats:
dataprop
EQINT (int, int) = {x:int} EQINT (x, x)
Say that we have a value v of type int(i) and we want to be
able to refer to i in our code directly. This can be done as follows:
val [i:int] EQINT() = eqint_make_int (x)
where eqint_make_int is a proof function of the following type;
prfun eqint_make_int {a:int} (x: int (a)): [a2:int] EQINT (a, a2)
There are also dataprops like EQBOOL and EQADDR in prelude/basics_dyn.sats
for extracting indices of the sorts bool and addr, respectively.