# Unpacking a value of existential type

**URL:** <https://discourse.ats-lang.org/t/unpacking-a-value-of-existential-type/817>\
**Category:** Google Group\
**Created:** [November 23, 2013, 12:26pm UTC](https://discourse.ats-lang.org/t/unpacking-a-value-of-existential-type/817 "2013-11-23T12:26:49Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [November 23, 2013, 12:26pm UTC](https://discourse.ats-lang.org/t/unpacking-a-value-of-existential-type/817/1 "2013-11-23T12:26:49Z")

</div>

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.