package lambdapi

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

Install

Dune Dependency

Authors

Maintainers

Sources

lambdapi-2.4.1.tbz
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a

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

Source file rangeMap_intf.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
38
(************************************************************************)
(* The λΠ-modulo Interactive Proof Assistant *)
(************************************************************************)

(************************************************************************)
(* λΠ-modulo serialization Toplevel *)
(* Copyright Inria -- Dual License LGPL 2.1 / GPL3+                     *)
(* Written by: F. Blanqui, E. J. Gallego Arias, F. Lefoulon             *)
(************************************************************************)
(* Status: Experimental                                                 *)
(************************************************************************)

module type S = sig
  (** Maps a position of the cursor (point) to the corresponding token of type
     'a in a given text editor with a .lp file open. *)
  type 'a t

  module Range : Range_intf.S

  (** The empty range map.*)
  val empty : 'a t

  (** [find pt map] returns the only (token, range) couple in map such that
     [pt] is a point within the mapped interval range. Requires [map] to be
     well-defined (see add). *)
  val find : Range.point -> 'a t -> (Range.t * 'a) option

  (** [add range token map] adds a mapping (key : [range], value : [token]) to
      [map].

      Requires all added keys to be non overlapping intervals to be
      well-defined. /!\ Does not ensure proper functionning if the added keys
      are overlapping intervals, e.g might change a previously added (key,
      element) couple or throw an error. *)
  val add : Range.t -> 'a -> 'a t -> 'a t

  val to_string : ('a -> string) -> 'a t -> string
end
OCaml

Innovation. Community. Security.