Vec
Types
Constructors
For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.
Functions
def length (xs : Vec a) : Int
def sum (xs : Vec Int) : Int
def absolute (x : Int) : Int
def contains (value : Int) (xs : Vec Int) : Bool
def differentFrom (value : Int) (xs : Vec Int) : Bool
def allDifferent (xs : Vec Int) : Bool
def differentExceptZero (value : Int) (xs : Vec Int) : Bool
def allDifferentExceptZero (xs : Vec Int) : Bool
def equalTo (value : Int) (xs : Vec Int) : Bool
def allEqual (xs : Vec Int) : Bool
def count (value : Int) (xs : Vec Int) : Int
def amongCount (allowed : Vec Int) (xs : Vec Int) : Int
def dot (coefficients : Vec Int) (xs : Vec Int) : Int
def element (index : Int) (xs : Vec Int) : Int
def increasingFrom (previous : Int) (xs : Vec Int) : Bool
def increasing (xs : Vec Int) : Bool
def strictlyIncreasingFrom (previous : Int) (xs : Vec Int) : Bool
def strictlyIncreasing (xs : Vec Int) : Bool
def toFloat (value : Int) : Float
def sumFloat (xs : Vec Float) : Float
def allTrue (xs : Vec Bool) : Bool
def anyTrue (xs : Vec Bool) : Bool
def setLexLe (left : Vec Bool) (right : Vec Bool) : Bool