package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install

dune-project
 Dependency

Authors

Maintainers

Sources

lambdapi-2.3.0.tbz
sha256=9b13c3121ef87cf4d3311a8a1db43db4be7f0e5e2a702fdaff04a3b3c432cb31
sha512=81e0760ca77cb862a5bdb8927aa37faf7141c4e2484a8163dad0a3eaa21cc691acb5f72279c78588c085f53dde4bd35186346378feac0ab55ac06a679cf2e60f

doc/src/lambdapi.lplib/string.ml.html

Source file string.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
module S = Stdlib.String
include S

let to_list : string -> char list =
 fun s ->
  let l = ref [] in
  S.iter (fun c -> l := c :: !l) s;
  List.rev !l

let of_list : char list -> string =
 fun l ->
  let b = Buffer.create 37 in
  List.iter (Buffer.add_char b) l;
  Buffer.contents b

let is_substring : string -> string -> bool =
 fun e s ->
  let len_e = S.length e in
  let len_s = S.length s in
  let rec is_sub i =
    if len_s - i < len_e then false
    else if S.sub s i len_e = e then true
    else is_sub (i + 1)
  in
  is_sub 0

let is_prefix : string -> string -> bool =
 fun p s ->
  let len_p = S.length p in
  let len_s = S.length s in
  len_p <= len_s && S.sub s 0 len_p = p

let for_all : (char -> bool) -> string -> bool =
 fun p s ->
  let len_s = S.length s in
  let rec for_all i = i >= len_s || (p (S.get s i) && for_all (i + 1)) in
  for_all 0