package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Module `Space.Vector`

val pretty : Format.formatter -> 'n vector -> unit

val zero : 'n Nat.succ Nat.nat -> 'n Nat.succ vector

The call zero n returns the 0 vector in 𝕂ⁿ.

val repeat : scalar -> 'n Nat.succ Nat.nat -> 'n Nat.succ vector

The call repeat x n returns a vector in 𝕂ⁿ which each dimension containing the scalar x.

val base : 
  'n Nat.succ Finite.finite ->
  'n Nat.succ Nat.nat ->
  'n Nat.succ vector

The call base i n returns the i-th base vector in the orthonormal space of 𝕂ⁿ. In other words, the returned vector contains zero except for the i-th coordinate, which contains one.

val get : 'n Finite.finite -> 'n vector -> scalar

The call get i m returns the i-th coefficient.

val set : 'n Finite.finite -> scalar -> 'n vector -> 'n vector

The call set i x v returns a new vector of the same linear space as v, and with the same coordinates, except for the i-th one, which is set to the scalar x.

val size : 'n vector -> 'n Nat.nat

The call size v for v a vector of 𝕂ⁿ returns n.

val norm : 'n vector -> scalar

The call norm v computes the ∞-norm of v, i.e the maximum of the absolute values of its coordinates.

val max : 'n vector -> 'n vector -> 'n vector

The call max l r returns a vector for which each coordinate is the maximum between the corresponding coordinates of l and r.

package frama-c

Module Space.Vector

Module `Space.Vector`