6a6259bf29
All checks were successful
ci/woodpecker/push/build Pipeline was successful
Use metalogic to generate meta term anti-quotations
The idea is for the Very_Deep_Interpretation
to source the shallow material,
and then update the checking and elaboration functions
of the term anti-quotations.
To achieve this, the mechanism of removing and reading the notations
(mixfixes) of the term-antiquotations, after the metalogic
is sourced, is used.
Example:
With shallow:
datatype "typ" = Isabelle_DOF_typ string ("@{typ _}")
Generate a datatype whose Constructor Isabelle_DOF_typ has
the notation @{typ ...}.
You get:
find_consts name:"Isabelle_DOF_typ"
find_consts
name: "Isabelle_DOF_typ"
found 1 constant(s):
Shallow_Interpretation.typ.Isabelle_DOF_typ :: "char list ⇒ typ"
With Deep:
no_notation "Isabelle_DOF_typ" ("@{typ _}")
consts Isabelle_DOF_typ :: "string ⇒ typ" ("@{typ _}")
The notation is removed and then added to the new Isabelle_DOF_typ constant.
You get:
find_consts name:"Isabelle_DOF_typ"
find_consts
name: "Isabelle_DOF_typ"
found 2 constant(s):
Deep_Interpretation.Isabelle_DOF_typ :: "char list ⇒ Core.typ"
Shallow_Interpretation.typ.Isabelle_DOF_typ :: "char list ⇒ Shallow_Interpretation.typ"
But only the Deep_Interpretation constant has the notation (mixfix).
Then new interpretation of term anti-quotations is available
for the user.
10 lines
308 B
Plaintext
10 lines
308 B
Plaintext
session "Isabelle_DOF-Proofs" (proofs) = "HOL-Proofs" +
|
|
options [document = false, record_proofs = 2, parallel_limit = 500, document_build = dof]
|
|
sessions
|
|
"Isabelle_DOF"
|
|
Metalogic_ProofChecker
|
|
theories
|
|
Isabelle_DOF.ontologies
|
|
Isabelle_DOF.Isa_DOF
|
|
Very_Deep_DOF
|
|
Reification_Test |