Quelle simple_print.ml Sprache: SML

(* 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"

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.