Skip to content
Check the Agda files

Union, Intersection, Set Difference and Further Operations on Indexed Sets #367

Sign in to view logs

Union, Intersection, Set Difference and Further Operations on Indexed Sets

Union, Intersection, Set Difference and Further Operations on Indexed Sets #367

Triggered via pull request October 7, 2025 09:48
@pmbittnerpmbittner
synchronize #92
isetops-fixed
Status Failure
Total duration 1m 46s
Artifacts –

check.yml

on: pull_request
build
1m 44s
build
Fit to window
Zoom out
Zoom in

Annotations

2 errors and 1 notice
build
Process completed with exit code 1.
build: src/Vatras/Framework/Variants.agda#L123
Ambiguous name A. It could refer to any one of A bound at /home/runner/work/Vatras/Vatras/src/Vatras/Framework/Variants.agda:110,19-20 Vatras.Data.EqIndexedSet.A bound at /home/runner/work/Vatras/Vatras/src/Vatras/Data/IndexedSet.lagda.md:688,7-8 A is in scope as * a variable bound at /home/runner/work/Vatras/Vatras/src/Vatras/Framework/Variants.agda:110,19-20 in conflict with * a generalizable variable Vatras.Data.EqIndexedSet.ISet.A brought into scope by - the opening of Vatras.Data.EqIndexedSet at /home/runner/work/Vatras/Vatras/src/Vatras/Framework/Variants.agda:111,15-39 - the opening of ISet at - the application of .#Vatras.Data.IndexedSet-12970533887692858968 at - its definition at /home/runner/work/Vatras/Vatras/src/Vatras/Data/IndexedSet.lagda.md:688,7-8 when scope checking A
build
The following files couldn't be checked because a dependency of them has errors: Vatras/Translation/Lang/VariantList-to-VT.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/OC/Show.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/VT/Encode.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/NADT.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/ADT/DeadElim.agda (depends on Vatras/Framework/Variants.agda) Vatras/Tutorial/B_Translation.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Lang/Gruler.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/FST/IncompleteOnRose.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/ADT-to-2CC.agda (depends on Vatras/Framework/Variants.agda) Vatras/Test/Test/VariantList-Completeness.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/CCC/Encode.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Lang/2CC/Util.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/CCC-to-NCC.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/NCC/ShrinkTo2.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/OC/Alternative.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/VT.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/LanguageMap.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/FST-to-VariantList.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/NCC-to-2CC.agda (depends on Vatras/Framework/Variants.agda) Vatras/Main.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/OC-to-2CC.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Lang/OC/IncompleteOnRose.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Lang/All/Fixed.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/VT-to-ADT.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/All.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/NCC-to-CCC.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/NCC/Rename.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/CCC/Properties.agda (depends on Vatras/Framework/Variants.agda) Vatras/Tutorial/C_Proofs.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Lang/OC/Subtree.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Lang/NCC/Util.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/ADT/WalkSemantics.agda (depends on Vatras/Framework/Variants.agda) Vatras/Test/Examples/Variants.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/2CC/Properties.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/FST-to-OC.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Test/Examples/CCC.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/2CC-to-ADT.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/2CC-to-NCC.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/FST.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Lang/OC/Util.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/VariantList-to-CCC.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Lang/NCC/Show.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/ADT/Rename.agda (depends on Vatras/Framework/Variants.agda) Vatras/Translation/Lang/VT/Rename.agda (depends on Vatras/Framework/Variants.agda) Vatras/Test/Experiments/FST-Experiments.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/2CC.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Lang/NCC.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Lang/FST/Properties.lagda.md (depends on Vatras/Framework/Variants.agda) Vatras/Test/Experiments/ADT-to-TikZ-Forest.agda (depends on Vatras/Framework/Variants.agda) Vatras/Lang/CCC/Show.agda (depends