Seq (p.jasmin.2026.03.0.doc.jasmin.jasmin.Jasmin.Seq)

val size : 'a1 list -> Datatypes.nat

val nilp : 'a1 list -> bool

val ohead : 'a1 list -> 'a1 option

val head : 'a1 -> 'a1 list -> 'a1

val behead : 'a1 list -> 'a1 list

val ncons : Datatypes.nat -> 'a1 -> 'a1 list -> 'a1 list

val nseq : Datatypes.nat -> 'a1 -> 'a1 list

val cat : 'a1 list -> 'a1 list -> 'a1 list

val rcons : 'a1 list -> 'a1 -> 'a1 list

val nth : 'a1 -> 'a1 list -> Datatypes.nat -> 'a1

val find : 'a1 Ssrbool.pred -> 'a1 list -> Datatypes.nat

val filter : 'a1 Ssrbool.pred -> 'a1 list -> 'a1 list

val count : 'a1 Ssrbool.pred -> 'a1 list -> Datatypes.nat

val has : 'a1 Ssrbool.pred -> 'a1 list -> bool

val all : 'a1 Ssrbool.pred -> 'a1 list -> bool

val drop : Datatypes.nat -> 'a1 list -> 'a1 list

val take : Datatypes.nat -> 'a1 list -> 'a1 list

val catrev : 'a1 list -> 'a1 list -> 'a1 list

val rev : 'a1 list -> 'a1 list

val eqseq : 
  Eqtype.Equality.coq_type ->
  Eqtype.Equality.sort list ->
  Eqtype.Equality.sort list ->
  bool

val eqseqP : 
  Eqtype.Equality.coq_type ->
  Eqtype.Equality.sort list Eqtype.eq_axiom

val coq_HB_unnamed_factory_1 : 
  Eqtype.Equality.coq_type ->
  Eqtype.Equality.sort list Eqtype.Coq_hasDecEq.axioms_

val coq_Datatypes_list__canonical__eqtype_Equality : 
  Eqtype.Equality.coq_type ->
  Eqtype.Equality.coq_type

val mem_seq : 
  Eqtype.Equality.coq_type ->
  Eqtype.Equality.sort list ->
  Eqtype.Equality.sort ->
  bool

type seq_eqclass = Eqtype.Equality.sort list

val pred_of_seq : 
  Eqtype.Equality.coq_type ->
  seq_eqclass ->
  Eqtype.Equality.sort Ssrbool.pred_sort

val seq_predType : 
  Eqtype.Equality.coq_type ->
  Eqtype.Equality.sort Ssrbool.predType

val allP : 
  Eqtype.Equality.coq_type ->
  Eqtype.Equality.sort Ssrbool.pred ->
  Eqtype.Equality.sort list ->
  Bool.reflect

val uniq : Eqtype.Equality.coq_type -> Eqtype.Equality.sort list -> bool

val index : 
  Eqtype.Equality.coq_type ->
  Eqtype.Equality.sort ->
  Eqtype.Equality.sort list ->
  Datatypes.nat

type bitseq = bool list

val mask : bitseq -> 'a1 list -> 'a1 list

val rem : 
  Eqtype.Equality.coq_type ->
  Eqtype.Equality.sort ->
  Eqtype.Equality.sort list ->
  Eqtype.Equality.sort list

val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list

val pmap : ('a1 -> 'a2 option) -> 'a1 list -> 'a2 list

val iota : Datatypes.nat -> Datatypes.nat -> Datatypes.nat list

val foldr : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2

val foldl : ('a2 -> 'a1 -> 'a2) -> 'a2 -> 'a1 list -> 'a2

val zip : 'a1 list -> 'a2 list -> ('a1 * 'a2) list

val unzip2 : ('a1 * 'a2) list -> 'a2 list

val all2 : ('a1 -> 'a2 -> bool) -> 'a1 list -> 'a2 list -> bool

val flatten : 'a1 list list -> 'a1 list