{-# OPTIONS --safe --cubical #-}
module OWL2.Corpus.Accepted.OBOGraph.Raw where
open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Corpus.Accepted.OBOGraph.Policy as Policy
open import OWL2.Elab
open import OWL2.Foundation.List
open import OWL2.Import.OBOGraph
open import OWL2.Import.OBOGraph.Raw
open import OWL2.OBOGraph.Syntax
open import OWL2.Raw hiding (SourcePath; sourcePath; rootPath; fieldPath; indexPath)
import OWL2.Check.Bundle as Bundle
import OWL2.Examples.OBOGraph.Json.AllValuesFromEdges as AllValuesFromEdges
import OWL2.Examples.OBOGraph.Json.CheckedKernelSmoke as CheckedKernelSmoke
import OWL2.Examples.OBOGraph.References as References
import OWL2.Kernel as K
versionedGraphOntologyIRI versionedGraphVersionIRI : RawIRI
versionedGraphOntologyIRI =
rawIRI "http://example.test/obograph/versioned"
versionedGraphVersionIRI =
rawIRI "http://example.test/obograph/versioned/1"
versionedGraph : Graph
versionedGraph =
graph
(present "http://example.test/obograph/versioned")
(present "http://example.test/obograph/versioned/1")
emptyMeta
[]
[]
[]
[]
[]
[]
[]
versionedGraphDocument : GraphDocument
versionedGraphDocument =
graphDocument (versionedGraph ∷ [])
versionedGraphRawOntologyIRI :
ontologyIRI (rawOntologyFromOBOGraph versionedGraphDocument) ≡
present versionedGraphOntologyIRI
versionedGraphRawOntologyIRI =
refl
versionedGraphRawVersionIRI :
versionIRI (rawOntologyFromOBOGraph versionedGraphDocument) ≡
present versionedGraphVersionIRI
versionedGraphRawVersionIRI =
refl
checkedKernelSmokeRawResult : OBOGraphRawImportResult
checkedKernelSmokeRawResult =
importOBOGraphRawStrict CheckedKernelSmoke.graphDocument
checkedKernelSmokeRawClean : Clean checkedKernelSmokeRawResult
checkedKernelSmokeRawClean =
tt
checkedKernelSmokeRawEvidence :
EvidenceAvailable checkedKernelSmokeRawResult
checkedKernelSmokeRawEvidence =
cleanEvidence
checkedKernelSmokeRawResult
checkedKernelSmokeRawClean
checkedKernelSmokeRaw : RawOntology
checkedKernelSmokeRaw =
rawImportSucceeded
checkedKernelSmokeRawResult
checkedKernelSmokeRawEvidence
checkedKernelSmokeRawAxiomCount :
listCount (axioms checkedKernelSmokeRaw) ≡ 8
checkedKernelSmokeRawAxiomCount =
refl
checkedKernelSmokeStructuralResult : ElaborationResult
checkedKernelSmokeStructuralResult =
elaborateStructuralKernelStrict checkedKernelSmokeRaw
checkedKernelSmokeStructuralClean :
Clean checkedKernelSmokeStructuralResult
checkedKernelSmokeStructuralClean =
tt
checkedKernelSmokeStructuralEvidence :
EvidenceAvailable checkedKernelSmokeStructuralResult
checkedKernelSmokeStructuralEvidence =
cleanEvidence
checkedKernelSmokeStructuralResult
checkedKernelSmokeStructuralClean
checkedKernelSmokeChecked : CheckedImport
checkedKernelSmokeChecked =
elaborationSucceeded
checkedKernelSmokeStructuralResult
checkedKernelSmokeStructuralEvidence
checkedKernelSmokeSound :
ElaboratesToCheckedImport
checkedKernelSmokeRaw
checkedKernelSmokeChecked
checkedKernelSmokeSound =
soundFromClean
checkedKernelSmokeStructuralResult
checkedKernelSmokeStructuralClean
checkedKernelSmokeComposedResult : OBOGraphCheckedImportResult
checkedKernelSmokeComposedResult =
importOBOGraphCheckedStrict CheckedKernelSmoke.graphDocument
checkedKernelSmokeComposedClean : Clean checkedKernelSmokeComposedResult
checkedKernelSmokeComposedClean =
tt
checkedKernelSmokeComposedEvidence :
EvidenceAvailable checkedKernelSmokeComposedResult
checkedKernelSmokeComposedEvidence =
cleanEvidence
checkedKernelSmokeComposedResult
checkedKernelSmokeComposedClean
checkedKernelSmokeComposedChecked : CheckedImport
checkedKernelSmokeComposedChecked =
checkedImportSucceeded
checkedKernelSmokeComposedResult
checkedKernelSmokeComposedEvidence
checkedKernelSmokeComposedCheckedFromClean : CheckedImport
checkedKernelSmokeComposedCheckedFromClean =
obographCheckedImportFromClean
checkedKernelSmokeComposedResult
checkedKernelSmokeComposedClean
checkedKernelSmokeComposedSourceEvidenceFromClean :
CheckedSourceEvidence checkedKernelSmokeComposedCheckedFromClean
checkedKernelSmokeComposedSourceEvidenceFromClean =
obographCheckedSourceEvidenceFromClean
checkedKernelSmokeComposedResult
checkedKernelSmokeComposedClean
checkedKernelSmokeComposedSound :
ImportsOBOGraphToChecked
CheckedKernelSmoke.graphDocument
checkedKernelSmokeComposedChecked
checkedKernelSmokeComposedSound =
soundFromClean
checkedKernelSmokeComposedResult
checkedKernelSmokeComposedClean
checkedKernelSmokeComposedRawAxiomCount :
listCount
(axioms (checkedRawOntology checkedKernelSmokeComposedSound)) ≡
8
checkedKernelSmokeComposedRawAxiomCount =
refl
checkedKernelSmokeClassCount :
K.classCount (signature checkedKernelSmokeChecked) ≡ 2
checkedKernelSmokeClassCount =
refl
checkedKernelSmokeComposedClassCount :
K.classCount (signature checkedKernelSmokeComposedChecked) ≡ 2
checkedKernelSmokeComposedClassCount =
refl
checkedKernelSmokeObjectPropertyCount :
K.objectPropertyCount (signature checkedKernelSmokeChecked) ≡ 1
checkedKernelSmokeObjectPropertyCount =
refl
checkedKernelSmokeIndividualCount :
K.individualCount (signature checkedKernelSmokeChecked) ≡ 2
checkedKernelSmokeIndividualCount =
refl
checkedKernelSmokeCheckedAxiomCount :
listCount (K.axioms (ontology checkedKernelSmokeChecked)) ≡ 8
checkedKernelSmokeCheckedAxiomCount =
refl
checkedKernelSmokeImportsRecorded :
requestedImports (sourceImportClosure checkedKernelSmokeChecked) ≡
imports checkedKernelSmokeRaw
checkedKernelSmokeImportsRecorded =
sourceImportsRecorded checkedKernelSmokeSound
checkedKernelSmokeBundleImportClosurePresent :
Bundle.importClosure (checkedEvidenceBundle checkedKernelSmokeChecked) ≡
present (Bundle.storedEvidenceOf
(sourceImportClosure checkedKernelSmokeChecked))
checkedKernelSmokeBundleImportClosurePresent =
refl
checkedKernelSmokePropertyRoleTraceRawPresent :
traceRawEvidence
(propertyRoleTrace
(sourcePropertyRoleEvidence checkedKernelSmokeChecked)) ≡
present
(checkedSourceTableRawTrace
checkedKernelSmokeRaw
refl
obographSource
refl)
checkedKernelSmokePropertyRoleTraceRawPresent =
refl
allValuesFromEdgesCheckedResult : OBOGraphCheckedImportResult
allValuesFromEdgesCheckedResult =
importOBOGraphCheckedStrict AllValuesFromEdges.graphDocument
allValuesFromEdgesCheckedClean :
Clean allValuesFromEdgesCheckedResult
allValuesFromEdgesCheckedClean =
tt
allValuesFromEdgesCheckedEvidence :
EvidenceAvailable allValuesFromEdgesCheckedResult
allValuesFromEdgesCheckedEvidence =
cleanEvidence
allValuesFromEdgesCheckedResult
allValuesFromEdgesCheckedClean
allValuesFromEdgesChecked : CheckedImport
allValuesFromEdgesChecked =
checkedImportSucceeded
allValuesFromEdgesCheckedResult
allValuesFromEdgesCheckedEvidence
allValuesFromEdgesCheckedFromClean : CheckedImport
allValuesFromEdgesCheckedFromClean =
obographCheckedImportFromClean
allValuesFromEdgesCheckedResult
allValuesFromEdgesCheckedClean
allValuesFromEdgesSound :
ImportsOBOGraphToChecked
AllValuesFromEdges.graphDocument
allValuesFromEdgesChecked
allValuesFromEdgesSound =
soundFromClean
allValuesFromEdgesCheckedResult
allValuesFromEdgesCheckedClean
allValuesFromEdgesRawAxiomCount :
listCount
(axioms (checkedRawOntology allValuesFromEdgesSound)) ≡
4
allValuesFromEdgesRawAxiomCount =
refl
allValuesFromEdgesClassCount :
K.classCount (signature allValuesFromEdgesChecked) ≡ 2
allValuesFromEdgesClassCount =
refl
allValuesFromEdgesObjectPropertyCount :
K.objectPropertyCount (signature allValuesFromEdgesChecked) ≡ 1
allValuesFromEdgesObjectPropertyCount =
refl
allValuesFromEdgesCheckedAxiomCount :
listCount (K.axioms (ontology allValuesFromEdgesChecked)) ≡ 4
allValuesFromEdgesCheckedAxiomCount =
refl
specialPredicateDocument : GraphDocument
specialPredicateDocument =
graphDocument (References.specialPredicateGraph ∷ [])
specialPredicateRawResult : OBOGraphRawImportResult
specialPredicateRawResult =
importOBOGraphRawStrict specialPredicateDocument
specialPredicateRawClean : Clean specialPredicateRawResult
specialPredicateRawClean =
tt
specialPredicateRawEvidence : EvidenceAvailable specialPredicateRawResult
specialPredicateRawEvidence =
cleanEvidence specialPredicateRawResult specialPredicateRawClean
specialPredicateRaw : RawOntology
specialPredicateRaw =
rawImportSucceeded specialPredicateRawResult specialPredicateRawEvidence
specialPredicateRawAxiomCount : listCount (axioms specialPredicateRaw) ≡ 3
specialPredicateRawAxiomCount =
refl
specialPredicateStructuralResult : ElaborationResult
specialPredicateStructuralResult =
elaborateStructuralKernelStrict specialPredicateRaw
specialPredicateStructuralClean : Clean specialPredicateStructuralResult
specialPredicateStructuralClean =
tt
specialPredicateStructuralEvidence :
EvidenceAvailable specialPredicateStructuralResult
specialPredicateStructuralEvidence =
cleanEvidence
specialPredicateStructuralResult
specialPredicateStructuralClean
specialPredicateChecked : CheckedImport
specialPredicateChecked =
elaborationSucceeded
specialPredicateStructuralResult
specialPredicateStructuralEvidence
specialPredicateClassCount :
K.classCount (signature specialPredicateChecked) ≡ 2
specialPredicateClassCount =
refl
specialPredicateCheckedAxiomCount :
listCount (K.axioms (ontology specialPredicateChecked)) ≡ 3
specialPredicateCheckedAxiomCount =
refl
declaredRelationDocument : GraphDocument
declaredRelationDocument =
graphDocument (References.declaredEdgeGraph ∷ [])
declaredRelationRawResult : OBOGraphRawImportResult
declaredRelationRawResult =
importOBOGraphRawStrict declaredRelationDocument
declaredRelationRawClean : Clean declaredRelationRawResult
declaredRelationRawClean =
tt
declaredRelationRawEvidence : EvidenceAvailable declaredRelationRawResult
declaredRelationRawEvidence =
cleanEvidence declaredRelationRawResult declaredRelationRawClean
declaredRelationRaw : RawOntology
declaredRelationRaw =
rawImportSucceeded declaredRelationRawResult declaredRelationRawEvidence
declaredRelationRawAxiomCount :
listCount (axioms declaredRelationRaw) ≡ 4
declaredRelationRawAxiomCount =
refl
declaredRelationStructuralResult : ElaborationResult
declaredRelationStructuralResult =
elaborateStructuralKernelStrict declaredRelationRaw
declaredRelationStructuralClean : Clean declaredRelationStructuralResult
declaredRelationStructuralClean =
tt
declaredRelationStructuralEvidence :
EvidenceAvailable declaredRelationStructuralResult
declaredRelationStructuralEvidence =
cleanEvidence
declaredRelationStructuralResult
declaredRelationStructuralClean
declaredRelationChecked : CheckedImport
declaredRelationChecked =
elaborationSucceeded
declaredRelationStructuralResult
declaredRelationStructuralEvidence
declaredRelationClassCount :
K.classCount (signature declaredRelationChecked) ≡ 2
declaredRelationClassCount =
refl
declaredRelationObjectPropertyCount :
K.objectPropertyCount (signature declaredRelationChecked) ≡ 1
declaredRelationObjectPropertyCount =
refl
declaredRelationCheckedAxiomCount :
listCount (K.axioms (ontology declaredRelationChecked)) ≡ 4
declaredRelationCheckedAxiomCount =
refl
knownObjectPropertyRawResult : OBOGraphRawImportResult
knownObjectPropertyRawResult =
importOBOGraphRawStrict Policy.knownObjectPropertyDocument
knownObjectPropertyRawClean : Clean knownObjectPropertyRawResult
knownObjectPropertyRawClean =
tt
knownObjectPropertyRawEvidence :
EvidenceAvailable knownObjectPropertyRawResult
knownObjectPropertyRawEvidence =
cleanEvidence
knownObjectPropertyRawResult
knownObjectPropertyRawClean
knownObjectPropertyRaw : RawOntology
knownObjectPropertyRaw =
rawImportSucceeded
knownObjectPropertyRawResult
knownObjectPropertyRawEvidence
knownObjectPropertyRawAxiomCount :
listCount (axioms knownObjectPropertyRaw) ≡ 1
knownObjectPropertyRawAxiomCount =
refl
knownObjectPropertyStructuralResult : ElaborationResult
knownObjectPropertyStructuralResult =
elaborateStructuralKernelStrict knownObjectPropertyRaw
knownObjectPropertyStructuralClean : Clean knownObjectPropertyStructuralResult
knownObjectPropertyStructuralClean =
tt
knownObjectPropertyStructuralEvidence :
EvidenceAvailable knownObjectPropertyStructuralResult
knownObjectPropertyStructuralEvidence =
cleanEvidence
knownObjectPropertyStructuralResult
knownObjectPropertyStructuralClean
knownObjectPropertyChecked : CheckedImport
knownObjectPropertyChecked =
elaborationSucceeded
knownObjectPropertyStructuralResult
knownObjectPropertyStructuralEvidence
knownObjectPropertyCount :
K.objectPropertyCount (signature knownObjectPropertyChecked) ≡ 1
knownObjectPropertyCount =
refl
knownObjectPropertyCheckedAxiomCount :
listCount (K.axioms (ontology knownObjectPropertyChecked)) ≡ 1
knownObjectPropertyCheckedAxiomCount =
refl
obographABoxNodeClass : String → Node
obographABoxNodeClass text =
node text absent classNode absent emptyMeta
obographABoxNodeIndividual : String → Node
obographABoxNodeIndividual text =
node text absent individualNode absent emptyMeta
obographABoxNodeObjectProperty : String → Node
obographABoxNodeObjectProperty text =
node text absent propertyNode (present objectProperty) emptyMeta
obographABoxGraph : Graph
obographABoxGraph =
graph
absent
absent
emptyMeta
(obographABoxNodeClass "A" ∷
obographABoxNodeIndividual "x" ∷
obographABoxNodeIndividual "y" ∷
obographABoxNodeObjectProperty "R" ∷ [])
(edge "x" "type" "A" emptyMeta ∷
edge "x" "R" "y" emptyMeta ∷ [])
[]
[]
[]
[]
[]
obographABoxDocument : GraphDocument
obographABoxDocument =
graphDocument (obographABoxGraph ∷ [])
obographABoxRawResult : OBOGraphRawImportResult
obographABoxRawResult =
importOBOGraphRawStrict obographABoxDocument
obographABoxRawClean : Clean obographABoxRawResult
obographABoxRawClean =
tt
obographABoxRawEvidence : EvidenceAvailable obographABoxRawResult
obographABoxRawEvidence =
cleanEvidence obographABoxRawResult obographABoxRawClean
obographABoxRaw : RawOntology
obographABoxRaw =
rawImportSucceeded obographABoxRawResult obographABoxRawEvidence
obographABoxRawAxiomCount : listCount (axioms obographABoxRaw) ≡ 6
obographABoxRawAxiomCount =
refl
obographABoxStructuralResult : ElaborationResult
obographABoxStructuralResult =
elaborateStructuralKernelStrict obographABoxRaw
obographABoxStructuralClean : Clean obographABoxStructuralResult
obographABoxStructuralClean =
tt
obographABoxStructuralEvidence :
EvidenceAvailable obographABoxStructuralResult
obographABoxStructuralEvidence =
cleanEvidence obographABoxStructuralResult obographABoxStructuralClean
obographABoxChecked : CheckedImport
obographABoxChecked =
elaborationSucceeded
obographABoxStructuralResult
obographABoxStructuralEvidence
obographABoxClassCount :
K.classCount (signature obographABoxChecked) ≡ 1
obographABoxClassCount =
refl
obographABoxObjectPropertyCount :
K.objectPropertyCount (signature obographABoxChecked) ≡ 1
obographABoxObjectPropertyCount =
refl
obographABoxIndividualCount :
K.individualCount (signature obographABoxChecked) ≡ 2
obographABoxIndividualCount =
refl
obographABoxCheckedAxiomCount :
listCount (K.axioms (ontology obographABoxChecked)) ≡ 6
obographABoxCheckedAxiomCount =
refl
metadataNodeA : Node
metadataNodeA =
node
"A"
(present "Class A")
classNode
absent
(meta
absent
("node comment" ∷ [])
[]
[]
[]
[]
false
[])
metadataNodeB : Node
metadataNodeB =
node "B" absent classNode absent emptyMeta
metadataEdge : Edge
metadataEdge =
edge
"A"
"is_a"
"B"
(meta
absent
[]
("EDGE:1" ∷ [])
[]
[]
[]
false
[])
metadataGraph : Graph
metadataGraph =
graph
absent
absent
(meta
(present "graph definition")
[]
[]
[]
[]
(propertyValue
"http://example.test/seeAlso"
"http://example.test/target"
(present "xsd:anyURI")
∷ [])
false
[])
(metadataNodeA ∷ metadataNodeB ∷ [])
(metadataEdge ∷ [])
[]
[]
[]
[]
[]
metadataDocument : GraphDocument
metadataDocument =
graphDocument (metadataGraph ∷ [])
metadataRawResult : OBOGraphRawImportResult
metadataRawResult =
importOBOGraphRawStrict metadataDocument
metadataRawClean : Clean metadataRawResult
metadataRawClean =
tt
metadataRawEvidence : EvidenceAvailable metadataRawResult
metadataRawEvidence =
cleanEvidence metadataRawResult metadataRawClean
metadataRaw : RawOntology
metadataRaw =
rawImportSucceeded metadataRawResult metadataRawEvidence
metadataRawOntologyAnnotationCount :
listCount (annotations metadataRaw) ≡ 2
metadataRawOntologyAnnotationCount =
refl
metadataRawAxiomCount :
listCount (axioms metadataRaw) ≡ 9
metadataRawAxiomCount =
refl
metadataStructuralResult : ElaborationResult
metadataStructuralResult =
elaborateStructuralKernelStrict metadataRaw
metadataStructuralClean : Clean metadataStructuralResult
metadataStructuralClean =
tt
metadataStructuralEvidence : EvidenceAvailable metadataStructuralResult
metadataStructuralEvidence =
cleanEvidence metadataStructuralResult metadataStructuralClean
metadataChecked : CheckedImport
metadataChecked =
elaborationSucceeded metadataStructuralResult metadataStructuralEvidence
seventhCheckedAnnotationCount :
{Sig : K.Signature} →
List (K.Annotated Sig (K.Axiom Sig)) →
ℕ
seventhCheckedAnnotationCount
(_ ∷ _ ∷ _ ∷ _ ∷ _ ∷ _ ∷ axiom ∷ axioms) =
listCount (K.itemAnnotations axiom)
seventhCheckedAnnotationCount _ =
0
metadataAnnotationPropertyCount :
K.annotationPropertyCount (signature metadataChecked) ≡ 5
metadataAnnotationPropertyCount =
refl
metadataDatatypeCount :
K.datatypeCount (signature metadataChecked) ≡ 1
metadataDatatypeCount =
refl
metadataIRICount :
K.iriCount (signature metadataChecked) ≡ 1
metadataIRICount =
refl
metadataOntologyAnnotationCount :
listCount (K.ontologyAnnotations (ontology metadataChecked)) ≡ 2
metadataOntologyAnnotationCount =
refl
metadataAnnotatedAxiomCount :
listCount (K.annotatedAxioms (ontology metadataChecked)) ≡ 9
metadataAnnotatedAxiomCount =
refl
metadataNodeAnnotationCount :
seventhCheckedAnnotationCount
(K.annotatedAxioms (ontology metadataChecked)) ≡ 2
metadataNodeAnnotationCount =
refl
metadataCheckedAxiomCount :
listCount (K.axioms (ontology metadataChecked)) ≡ 9
metadataCheckedAxiomCount =
refl
compatibilityLossyPropertyValue : PropertyValue
compatibilityLossyPropertyValue =
propertyValue
"http://example.test/date"
"2026-06-27"
(present "xsd:date")
compatibilityLossyMetadataGraph : Graph
compatibilityLossyMetadataGraph =
graph
absent
absent
(meta
absent
[]
[]
[]
[]
(compatibilityLossyPropertyValue ∷ [])
false
[])
[]
[]
[]
[]
[]
[]
[]
compatibilityLossyMetadataDocument : GraphDocument
compatibilityLossyMetadataDocument =
graphDocument (compatibilityLossyMetadataGraph ∷ [])
compatibilityLossyMetadataRawResult : OBOGraphRawImportResult
compatibilityLossyMetadataRawResult =
importOBOGraphRawCompatibility compatibilityLossyMetadataDocument
compatibilityLossyMetadataRawClean :
Clean compatibilityLossyMetadataRawResult
compatibilityLossyMetadataRawClean =
tt
compatibilityLossyMetadataRawEvidence :
EvidenceAvailable compatibilityLossyMetadataRawResult
compatibilityLossyMetadataRawEvidence =
cleanEvidence
compatibilityLossyMetadataRawResult
compatibilityLossyMetadataRawClean
compatibilityLossyMetadataRaw : RawOntology
compatibilityLossyMetadataRaw =
rawImportSucceeded
compatibilityLossyMetadataRawResult
compatibilityLossyMetadataRawEvidence
firstRawAnnotationNestedCount : List RawAnnotation → ℕ
firstRawAnnotationNestedCount [] =
0
firstRawAnnotationNestedCount (rawAnnotation annotations property value ∷ rest) =
listCount annotations
compatibilityLossyMetadataRawOntologyAnnotationCount :
listCount (annotations compatibilityLossyMetadataRaw) ≡ 1
compatibilityLossyMetadataRawOntologyAnnotationCount =
refl
compatibilityLossyMetadataRawNestedWarningCount :
firstRawAnnotationNestedCount
(annotations compatibilityLossyMetadataRaw) ≡ 1
compatibilityLossyMetadataRawNestedWarningCount =
refl
compatibilityLossyMetadataRawAxiomCount :
listCount (axioms compatibilityLossyMetadataRaw) ≡ 3
compatibilityLossyMetadataRawAxiomCount =
refl
compatibilityLossyMetadataStructuralResult : ElaborationResult
compatibilityLossyMetadataStructuralResult =
elaborateStructuralKernelStrict compatibilityLossyMetadataRaw
compatibilityLossyMetadataStructuralClean :
Clean compatibilityLossyMetadataStructuralResult
compatibilityLossyMetadataStructuralClean =
tt
compatibilityLossyMetadataStructuralEvidence :
EvidenceAvailable compatibilityLossyMetadataStructuralResult
compatibilityLossyMetadataStructuralEvidence =
cleanEvidence
compatibilityLossyMetadataStructuralResult
compatibilityLossyMetadataStructuralClean
compatibilityLossyMetadataChecked : CheckedImport
compatibilityLossyMetadataChecked =
elaborationSucceeded
compatibilityLossyMetadataStructuralResult
compatibilityLossyMetadataStructuralEvidence
firstCheckedOntologyAnnotationNestedCount :
{Sig : K.Signature} →
List (K.Annotation Sig) →
ℕ
firstCheckedOntologyAnnotationNestedCount [] =
0
firstCheckedOntologyAnnotationNestedCount
(K.annotation annotations property value ∷ rest) =
listCount annotations
compatibilityLossyMetadataAnnotationPropertyCount :
K.annotationPropertyCount
(signature compatibilityLossyMetadataChecked) ≡ 2
compatibilityLossyMetadataAnnotationPropertyCount =
refl
compatibilityLossyMetadataDatatypeCount :
K.datatypeCount (signature compatibilityLossyMetadataChecked) ≡ 1
compatibilityLossyMetadataDatatypeCount =
refl
compatibilityLossyMetadataOntologyAnnotationCount :
listCount
(K.ontologyAnnotations (ontology compatibilityLossyMetadataChecked)) ≡ 1
compatibilityLossyMetadataOntologyAnnotationCount =
refl
compatibilityLossyMetadataCheckedNestedWarningCount :
firstCheckedOntologyAnnotationNestedCount
(K.ontologyAnnotations
(ontology compatibilityLossyMetadataChecked)) ≡ 1
compatibilityLossyMetadataCheckedNestedWarningCount =
refl
compatibilityLossyMetadataCheckedAxiomCount :
listCount (K.axioms (ontology compatibilityLossyMetadataChecked)) ≡ 3
compatibilityLossyMetadataCheckedAxiomCount =
refl