# before existential quantifiers; <lin,prf>

Google Group
1

fun{}
LAgmat_vtakeout_row
{a:t0p}{mo:mord}{m,n:int}
(
!LAgmat(a, mo, m, n)
, i: natLt(m), d: &int? >> int(d)
) :
#[
l:addr;d:int
] (
gvector_v (a, l, n, d)
, gvector_v (a, l, n, d) -<lin,prf> void
| ptr (l)
) // end of [LAgmat_vtakeout_row]

Or may it isn’t new, but I can’t remember what the # would mean before
existential quantifiers.

Also, in this example, it is not clear to me why two views are returned
(nor do I have a great grasp of what the sorts and do).

  1. gvector_v (a, l, n, d)
  2. gvector_v (a, l, n, d) -<lin,prf> void
2

Thanks, yes, I’m pretty sure this is a road I have wandered down before
w.r.t. “#[”. That’s a great explanation.

3

The #[…] in existential qualifiers means that that variable can be
referenced in function parameters. Notice the ‘d’ is referenced in the type
of the ‘d’ argument. Without the ‘#’ this would be an error.

The two views returned are:

  1. This is a view saying you have a vector.
  2. This is a linear proof function that can be used to consume the first
    view. A linear proof function is consumed when it is called as well. This
    idiom is often used for ‘borrowing’ pointers from other structures. You get
    a proof of the borrowed data and a linear proof function that consumes that
    proof.

http://www.bluishcoder.co.nz