pub fn check_chrvec
[
N : Nat,
$S,
@D
]
( c : list[bool[N] $S @D] $pre @public
)
-> () $pre @public
where
Field[N]
Assertion that the argument list is a characteristic vector, i.e., contains exactly one true value. Assumes that the length of the list is less than the modulus.
pub fn chrvec
[
N : Nat,
$S,
@D
]
( n : uint[18446744073709551616] $pre @public,
ind : uint[N] $S @D
)
-> list[bool[N] $S @D] $pre @public
where
Field[N]
The characteristic vector of the natural number given as the second argument, having length given as the first argument. If the second argument is not less than the first argument then the result consists of falses only.
pub fn chrvec_list_pre
[
N : Nat,
@D
]
( n : uint[18446744073709551616] $pre @D,
is : list[uint[N] $pre @D] $pre @D
)
-> list[bool[N] $pre @D] $pre @D
The characteristic vector of the given list of indices in
$pre
, having length given as the first argument. Fails if the given list contains any number not less than the first argument.
pub fn chrvec_lt
[
N : Nat,
$S,
@D
]
( n : uint[18446744073709551616] $pre @public,
ind : uint[N] $S @D
)
-> list[bool[N] $S @D] $pre @public
where
Field[N]
The characteristic vector of being less than the natural number given as the second argument, having length given as the first argument.
pub fn element
[
N : Nat,
$S,
@D
]
( text : list[uint[N] $S @D] $pre @public,
ind : uint[N] $S @D
)
-> uint[N] $S @D
where
Field[N]
The element of the list given as the first argument located at the position given as the second argument. Fails if the position is out of bounds of the list.
pub fn segment
[
N : Nat,
$S,
@D
]
( text : list[uint[N] $S @D] $pre @public,
ind : uint[N] $S @D,
m : uint[18446744073709551616] $pre @public
)
-> list[uint[N] $S @D] $pre @public
where
Field[N]
A segment of the list given as the first argument, starting from the index given as the second argument and having length given as the third argument. Fails if the segment would extend beyond the end of the given list.