package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.5.1.tbz
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf
doc/src/lambdapi.lplib/range_intf.ml.html
Source file range_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 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
(************************************************************************) (* 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 for points and intervals. Used to determine if a cursor is in the range of a specific token, which is an interval of points (cursor positions). The presence of t and compare make [RangeType] an [OrderedType] (in the sense of [Map]). For now, the useful modules out of this library are [Range] and [RangeMap]. *) module type S = sig type point type t (** [make_point ln col] creates a point with line [ln] and column [col]. *) val make_point : int -> int -> point (** [make_interval s e] creates an interval with start [s] and end [e]. Requires the interval to be well defined (e.g with start < finish) or it will assert *) val make_interval : point -> point -> t val line : point -> int val column : point -> int val interval_start : t -> point val interval_end : t -> point (** Type for the position of a cursor relative to an interval. *) type cmp = | Before | In | After (** [in_range pt i] returns [Before], [In] or [After] depending on the position of the point [pt] relative to the interval [i].*) val in_range : point -> t -> cmp (** Comparison over intervals. An interval is considered "smaller" than another if its ending point is before the starting point of the other. Intervals need to be well defined (i.e returned by make_interval). Two intervals are considered equal if one is included in the other. In any other case, overlapping intervals can't be compared and will throw an error. *) val compare : t -> t -> int val point_to_string : point -> string val interval_to_string : t -> string (** [translate i ds df] returns the interval [i] with its starting point translated by [ds] and finishing point translated by [df]. Will throw an error if the resulting interval is not well-defined (see make_interval). Only translates column-wise, does not modify the line coordinates of the extremity points. *) val translate : t -> int -> int -> t end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>