package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.14.0.tar.gz
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c
doc/src/coq-core.gramlib/plexing.ml.html
Source file plexing.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
(* camlp5r *) (* plexing.ml,v *) (* Copyright (c) INRIA 2007-2017 *) type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te LStream.t module type S = sig type te type 'c pattern val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option val tok_pattern_strings : 'c pattern -> string * string option val tok_func : te lexer_func val tok_using : 'c pattern -> unit val tok_removing : 'c pattern -> unit val tok_match : 'c pattern -> te -> 'c val tok_text : 'c pattern -> string (* State for the comments, at some point we should make it functional *) module State : sig type t val init : unit -> t val set : t -> unit val get : unit -> t val drop : unit -> unit val get_comments : t -> ((int * int) * string) list val set_loc_offset : int -> unit end end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>