fsdoc: no-summary-found
fsdoc: no-comment-found
Functions on list with a pure specification val map2:#a1:Type -> #a2:Type -> #b:Type -> f:Unidentified product: [a1] Unidentified product: [a2] b -> l1:list a1 -> l2:list a2 -> (Pure (list b) ((requires (==(length l1, length l2)))) ((ensures ((fun _ -> True)))) (decreases l1))[map2] takes a pair of list of the same length [x1; ...; xn] [y1; ... ; yn] and return the list [f x1 y1; ... ; f xn yn]
val map3:#a1:Type -> #a2:Type -> #a3:Type -> #b:Type -> f:Unidentified product: [a1] Unidentified product: [a2] Unidentified product: [a3] b -> l1:list a1 -> l2:list a2 -> l3:list a3 -> (Pure (list b) ((requires (let n = length l1 in (/\(==(n, length l2), ==(n, length l3)))))) ((ensures ((fun _ -> True)))) (decreases l1))[map3] takes three lists of the same length [x1; ...; xn][y1; ... ; yn] [z1; ... ; zn] and return the list [f x1 y1 z1; ... ; f xn yn zn]
val zip:#a1:Type -> #a2:Type -> l1:list a1 -> l2:list a2 -> (Pure (list (*(a1, a2))) ((requires (let n = length l1 in ==(n, length l2)))) ((ensures ((fun _ -> True)))))[zip] takes a pair of list of the same length and returns the list of index-wise pairs
val zip3:#a1:Type -> #a2:Type -> #a3:Type -> l1:list a1 -> l2:list a2 -> l3:list a3 -> (Pure (list (*(*(a1, a2), a3))) ((requires (let n = length l1 in /\(==(n, length l2), ==(n, length l3))))) ((ensures ((fun _ -> True)))))[zip3] takes a 3-tuple of list of the same length and returns the list of index-wise 3-tuples