package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c

doc/src/coq-core.lib/cAst.ml.html

Source file cAst.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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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)         *)
(************************************************************************)

(** The ast type contains generic metadata for AST nodes. *)
type 'a t = {
  v   : 'a;
  loc : Loc.t option;
}

let make ?loc v = { v; loc }

let map f n = { n with v = f n.v }
let map_with_loc f n = { n with v = f ?loc:n.loc n.v }
let map_from_loc f l =
  let loc, v = l in
  { v = f ?loc v ; loc }

let with_val f n = f n.v
let with_loc_val f n = f ?loc:n.loc n.v

let eq f x y = f x.v y.v

module Smart = struct
  let map f n =
    let v' = f n.v in
    if v' == n.v then n
    else {n with v=v'}
end
OCaml

Innovation. Community. Security.