ATSLIB/contrib/libfloats/lavector

LAgvec

Synopsis

stadef LAgvec = LAgvec_vtype

vtypedef LAgvec
  (a:t@ype, n: int) = [l:addr] LAgvec(a, l, n)

LAgvec_vtype

Synopsis

absvtype
LAgvec_vtype
  (a:t@ype, l: addr, n: int) = ptr(l)

lemma_LAgvec_param

Synopsis

praxi
lemma_LAgvec_param
  {a:t0p}{n:int}
  (V: !LAgvec(a, n)): [n >= 0] void

LAgvec_size

Synopsis

fun{}
LAgvec_size
  {a:t0p}{n:int}(!LAgvec(a, n)): int(n)

LAgvec_vtakeout_vector

Synopsis

fun{}
LAgvec_vtakeout_vector
  {a:t0p}{n:int}
(
  !LAgvec(a, n), &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 [LAgvec_vtakeout_vector]

LAgvec_get_at

Synopsis

fun{a:t0p}
LAgvec_get_at{n:int}
  (V: !LAgvec(a, n), i: natLt(n)): (a)

LAgvec_set_at

Synopsis

fun{a:t0p}
LAgvec_set_at{n:int}
  (V: !LAgvec(a, n), i: natLt(n), x: a): void

LAgvec_getref_at

Synopsis

fun{a:t0p}
LAgvec_getref_at{n:int}
  (V: !LAgvec(a, n), i: natLt(n)) : cPtr1(a)

fprint_LAgvec

Synopsis

fun{a:t0p}
fprint_LAgvec{n:int}
  (out: FILEref, V: !LAgvec(a, n)): void

fprint_LAgvec$sep

Synopsis

fun{}
fprint_LAgvec$sep (FILEref): void

fprint_LAgvec_sep

Synopsis

fun{a:t0p}
fprint_LAgvec_sep{n:int}
  (out: FILEref, V: !LAgvec(a, n), sep: string): void

LAgvec_split

Synopsis

fun{a:t0p}
LAgvec_split
  {n:int}{i:nat | i <= n}
  (LAgvec(a, n), int(i)): (LAgvec(a, i), LAgvec(a, n-i))

LAgvec_tabulate

Synopsis

fun{a:t0p}
LAgvec_tabulate {n:nat} (n: int n): LAgvec(a, n)

LAgvec_tabulate$fopr

Synopsis

fun{a:t0p}
LAgvec_tabulate$fopr (i: int): a

LAgvec_inner

Synopsis

fun{a:t0p}
LAgvec_inner{n:int}
  (A: !LAgvec(a, n), B: !LAgvec(a, n)): a(*innerprod*)

LAgvec_scal

Synopsis

fun{a:t0p}
LAgvec_scal{n:int}
  (alpha: a, X: !LAgvec(a, n) >> _) : void

scal_LAgvec

Synopsis

fun{a:t0p}
scal_LAgvec{n:int}
  (alpha: a, X: !LAgvec(a, n)): LAgvec(a, n)

LAgvec_copy

Synopsis

fun{a:t0p}
LAgvec_copy{n:int}
(
  X: !LAgvec(a, n)
, Y: !LAgvec(a?, n) >> LAgvec(a, n)
) : void // endfun

copy_LAgvec

Synopsis

fun{a:t0p}
copy_LAgvec
  {n:int}(X: !LAgvec(a, n)): LAgvec(a, n)

LAgvec_swap

Synopsis

fun{a:t0p}
LAgvec_swap{n:int}
(
  X: !LAgvec(a, n) >> _
, Y: !LAgvec(a, n) >> _
) : void // endfun

LAgvec_ax1y

Synopsis

fun{a:t0p}
LAgvec_ax1y{n:int}
(
  alpha: a, X: !LAgvec(a, n), Y: !LAgvec(a, n) >> _
) : void // [LAgvec_ax1y]

LAgvec_axby

Synopsis

fun{a:t0p}
LAgvec_axby{n:int}
(
  alpha: a, X: !LAgvec(a, n), beta: a, Y: !LAgvec(a, n) >> _
) : void // [LAgvec_axby]

Overloaded Symbols

[]

Synopsis

overload [] with LAgvec_get_at

overload [] with LAgvec_set_at

.size

Synopsis

overload .size with LAgvec_size

fprint

Synopsis

overload fprint with fprint_LAgvec

This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi.