(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
(** Lazy AST node wrapper. Only used for [glob_constr] as of today. *)
type ('a, _) thunk =
| Value : 'a -> ('a, 'b) thunk
| Thunk : 'a Lazy.t -> ('a, [ `thunk ]) thunk
type ('a, 'b) t = ('a, 'b) thunk CAst.t
val get : ('a, 'b) t -> 'a val get_thunk : ('a, 'b) thunk -> 'a
val make : ?loc:Loc.t -> 'a -> ('a, 'b) t val delay : ?loc:Loc.t -> (unit -> 'a) -> ('a, [ `thunk ]) t val force : ('a, 'b) t -> ('a, 'b) t
valmap : ('a -> 'b) -> ('a, 'c) t -> ('b, 'c) t val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> ('b, 'c) t val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> ('b, 'c) t
val with_val : ('a -> 'b) -> ('a, 'c) t -> 'b val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> 'b
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
