Quelle drop.txt Sprache: Text

When you start byte-compiled Rocq toplevel:

  rlwrap bin/coqtop.byte

then if you type:

  Drop.

you will decend from Rocq toplevel down to Ocaml toplevel.
So if you want to learn:
- the current values of some global variables you are interested in
- or see what happens when you invoke certain functions
this is the place where you can do that.

When you try to print values belonging to abstract data types:

  # let sigma, env = Lemmas.get_current_context ();;

  val sigma : Evd.evar_map = <abstr>
  val env : Environ.env = <abstr>

  # Typeops.infer env (snd (Pretyping.understand_tcc env sigma (Constrintern.intern_constr env (Procq.parse_string Procq.Constr.lconstr "plus"))));;

  - : Environ.unsafe_judgment = {Environ.uj_val = <abstr>; uj_type = <abstr>}

the printed values are not very helpful.

One way how to deal with that is to load the corresponding printers:

  # #use "dev/include";;

Consequently, the result of:

  # Typeops.infer env (snd (Pretyping.understand_tcc env sigma (Constrintern.intern_constr env (Procq.parse_string Procq.Constr.lconstr "plus"))));;

will be printed as:

  - : Environ.unsafe_judgment = Nat.add : nat -> nat -> nat

which makes more sense.

To be able to understand the meaning of the data types,
sometimes the best option is to turn those data types from abstract to concrete
and look at them without any kind of pretty printing.

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

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.