Introduce some deliberate errors for testing #7
Annotations
6 errors, 2 warnings, and 1 notice
|
src/Framework/Relation/Expressiveness.lagda.md#L4
The name of the top level module does not match the file name. The
module ramework.Relation.Expressiveness should be defined in one of
the following files:
/nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/ramework/Relation/Expressiveness.agda
/nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/ramework/Relation/Expressiveness.lagda
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/ramework/Relation/Expressiveness.agda
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/ramework/Relation/Expressiveness.lagda
/nix/store/s6774vfjza5r4dywxi8sgkdmq11nijsj-Agda-2.6.3-data/share/ghc-9.2.7/x86_64-linux-ghc-9.2.7/Agda-2.6.3/lib/prim/ramework/Relation/Expressiveness.agda
/nix/store/s6774vfjza5r4dywxi8sgkdmq11nijsj-Agda-2.6.3-data/share/ghc-9.2.7/x86_64-linux-ghc-9.2.7/Agda-2.6.3/lib/prim/ramework/Relation/Expressiveness.lagda
|
|
src/Framework/Proof/Soundness.lagda.md#L19
Unsolved metas at the following locations:
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Framework/Relation/Configuration.lagda.md:46,12-13
when scope checking the declaration
open import Framework.Relation.Configuration using (_⊢_≣ᶜ_;
≣ᶜ-IsEquivalence; ≣ᶜ-congruent)
|
|
src/Framework/Proof/Completeness.lagda.md#L14
The name of the top level module does not match the file name. The
module ramework.Relation.Expressiveness should probably be named
Framework.Relation.Expressiveness
when scope checking the declaration
open import Framework.Relation.Expressiveness
|
|
src/Framework/Proof/Translation.lagda.md#L34
The name of the top level module does not match the file name. The
module ramework.Relation.Expressiveness should probably be named
Framework.Relation.Expressiveness
when scope checking the declaration
open import Framework.Relation.Expressiveness
|
|
src/Framework/Properties/Soundness.lagda.md#L29
Unsolved metas at the following locations:
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Framework/Relation/Configuration.lagda.md:46,12-13
when scope checking the declaration
open import Framework.Relation.Configuration using (≣ᶜ-setoid)
|
|
src/Framework/V2/TODO.lagda.md#L48
(R : (F → S) → Set) → Set₁ should be a sort, but it isn't
when checking that the expression VariabilityLanguage V F S has
type _10
|
|
src/Framework/Relation/Expression.lagda.md#L8
The module Data.Product doesn't export the following:\n asd\nwhen scope checking the declaration\n open import Data.Product using (_,_; ∃-syntax; Σ-syntax; _×_; asd)\n
|
|
src/Framework/Definitions.lagda.md#L11
The module Data.Bool doesn't export the following:\n asd\nwhen scope checking the declaration\n open import Data.Bool using (Bool; asd)\n
|
|
The following files couldn't be checked because a dependency of them has errors:
Test/Experiments/OC-to-BCC.agda (depends on Framework/Proof/Translation.lagda.md)
Translation/CCC-to-BCC.lagda.md (depends on Framework/Proof/Translation.lagda.md)
Lang/BCC.lagda.md (depends on Framework/Proof/Translation.lagda.md)
Lang/BigStep.lagda.md (depends on Framework/Proof/Translation.lagda.md)
Main.agda (depends on Framework/Proof/Translation.lagda.md)
Translation/VariantList-to-CCC.lagda.md (depends on Framework/Properties/Soundness.lagda.md)
Translation/BCC-to-CCC.lagda.md (depends on Framework/Proof/Translation.lagda.md)
Test/Test/VariantList-Completeness.agda (depends on Framework/Proof/Translation.lagda.md)
Test/UnitTest.agda (depends on Framework/Proof/Translation.lagda.md)
Test/Experiments/CCC-to-BCC.agda (depends on Framework/Proof/Translation.lagda.md)
Translation/OC-to-BCC.lagda.md (depends on Framework/Proof/Translation.lagda.md)
Translation/LanguageMap.lagda.md (depends on Framework/Proof/Translation.lagda.md)
Lang/VariantList.lagda.md (depends on Framework/Properties/Soundness.lagda.md)
|
The logs for this run have expired and are no longer available.
Loading