Quelle canonical.ml Sprache: SML

(************************************************************************)
(*         *      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)         *)
(************************************************************************)
open Libobject
open Structures

let open_canonical_structure (o,_) =
  let env = Global.env () in
  let sigma = Evd.from_env env in
  Instance.register env sigma ~warn:false o

let cache_canonical_structure (o,_) =
  let env = Global.env () in
  let sigma = Evd.from_env env in
  Instance.register ~warn:true env sigma o

let discharge_canonical_structure (x, local) =
  let gref = Instance.repr x in
  if local || (Globnames.isVarRef gref && Global.is_in_section gref) then None
  else Some (x, local)

let canon_cat = create_category "canonicals"

let inCanonStruc : Instance.t * bool -> obj =
  declare_object {(default_object "CANONICAL-STRUCTURE") with
                  open_function = simple_open ~cat:canon_cat open_canonical_structure;
                  cache_function = cache_canonical_structure;
                  subst_function = (fun (subst,(c,local)) -> Instance.subst subst c, local);
                  classify_function = (fun x -> Substitute);
                  discharge_function = discharge_canonical_structure }

let add_canonical_structure x = Lib.add_leaf (inCanonStruc x)

let declare_canonical_structure ?(local=false) ref =
  let env = Global.env () in
  let sigma = Evd.from_env env in
  add_canonical_structure (Instance.make env sigma ref, local)

quality100%

¤ Dauer der Verarbeitung: 0.4 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.