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/tuto1_plugin/simple_print.ml.html

Source file simple_print.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
(* A more advanced example of how to explore the structure of terms of
  type constr is given in the coq-dpdgraph plugin. *)

let simple_body_access ~opaque_access gref =
  let open Names.GlobRef in
  match gref with
  | VarRef _ ->
    failwith "variables are not covered in this example"
  | IndRef _ ->
    failwith "inductive types are not covered in this example"
  | ConstructRef _ ->
    failwith "constructors are not covered in this example"
  | ConstRef cst ->
    let cb = Environ.lookup_constant cst (Global.env()) in
    (* most commands should not use body_of_constant_body and opaque accessors,
       but for printing it's ok *)
    match Global.body_of_constant_body opaque_access cb with
    | Some(e, _, _) -> EConstr.of_constr e
    | None -> failwith "This term has no value"