package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/src/rocq-runtime.pretyping/evaluable.ml.html

Source file evaluable.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
(************************************************************************)
(*         *      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)         *)
(************************************************************************)

(** Evaluable references (whose transparency can be controlled) *)

open Names

type t =
  | EvalVarRef of Id.t
  | EvalConstRef of Constant.t
  | EvalProjectionRef of Projection.Repr.t

let map fvar fcst fprj = function
  | EvalVarRef v -> EvalVarRef (fvar v)
  | EvalConstRef c -> EvalConstRef (fcst c)
  | EvalProjectionRef p -> EvalProjectionRef (fprj p)

let equal env er1 er2 =
  er1 == er2 ||
  match er1, er2 with
  | EvalVarRef v1, EvalVarRef v2 ->
      Id.equal v1 v2
  | EvalConstRef c1, EvalConstRef c2 ->
      Environ.QConstant.equal env c1 c2
  | EvalProjectionRef p1, EvalProjectionRef p2 ->
      Environ.QProjection.Repr.equal env p1 p2
  | _ -> false

let to_kevaluable : t -> Conv_oracle.evaluable = fun er ->
  match er with
  | EvalVarRef v -> Conv_oracle.EvalVarRef v
  | EvalConstRef c -> Conv_oracle.EvalConstRef c
  | EvalProjectionRef p -> Conv_oracle.EvalProjectionRef p