Skip to content
Lint

arch-split Refine up to Invariants_H for X64 #209

Sign in to view logs

arch-split Refine up to Invariants_H for X64

arch-split Refine up to Invariants_H for X64 #209

GitHub Actions / File annotations for theory linter succeeded Jan 6, 2025 in 0s

File annotations for theory linter

Annotations

Check failure on line 19 in proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy

See this annotation in the file changed.

@github-actions github-actions / File annotations for theory linter

Axioms 

Locales or definitions should usually be preferred to axioms, because axioms may make the logic inconsistent. Merely introducing a new constant (without new laws) is fine, though.

Check failure on line 19 in proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy

See this annotation in the file changed.

@github-actions github-actions / File annotations for theory linter

Axioms 

Locales or definitions should usually be preferred to axioms, because axioms may make the logic inconsistent. Merely introducing a new constant (without new laws) is fine, though.
View more details on GitHub Actions