extracted/listb.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Relations
   6
   7 open Nat
   8
   9 open Hints_declaration
  10
  11 open Core_notation
  12
  13 open Pts
  14
  15 open Logic
  16
  17 open Types
  18
  19 open List
  20
  21 open Sets
  22
  23 open Deqsets
  24
  25 (** val isnilb : 'a1 List.list -> Bool.bool **)
  26 let rec isnilb = function
  27 | List.Nil -> Bool.True
  28 | List.Cons (hd0, tl) -> Bool.False
  29
  30 (** val memb : Deqsets.deqSet -> __ -> __ List.list -> Bool.bool **)
  31 let rec memb s x = function
  32 | List.Nil -> Bool.False
  33 | List.Cons (a, tl) -> Bool.orb (Deqsets.eqb s x a) (memb s x tl)
  34
  35 (** val uniqueb : Deqsets.deqSet -> __ List.list -> Bool.bool **)
  36 let rec uniqueb s = function
  37 | List.Nil -> Bool.True
  38 | List.Cons (a, tl) -> Bool.andb (Bool.notb (memb s a tl)) (uniqueb s tl)
  39
  40 (** val unique_append :
  41     Deqsets.deqSet -> __ List.list -> __ List.list -> __ List.list **)
  42 let rec unique_append s l1 l2 =
  43   match l1 with
  44   | List.Nil -> l2
  45   | List.Cons (a, tl) ->
  46     let r = unique_append s tl l2 in
  47     (match memb s a r with
  48      | Bool.True -> r
  49      | Bool.False -> List.Cons (a, r))
  50
  51 (** val exists : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
  52 let rec exists p = function
  53 | List.Nil -> Bool.False
  54 | List.Cons (h, t) -> Bool.orb (p h) (exists p t)
  55