package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
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
(* camlp5r *) (* plexing.ml,v *) (* Copyright (c) INRIA 2007-2017 *) type 'te lexer_func = ?loc:Loc.t -> ?fix_loc:(Loc.t -> 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_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 end end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>