Skip to content

Commit 439cf3b

Browse files
committed
fix(verification): import Data.Nat for LTE in Idris2 trust proofs
AxiomPolicyOrdering and TrustLevelSoundness use LTE/LTESucc/LTEZero (from Data.Nat) without importing it. Verified: idris2 --check exits 0 for both. https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
1 parent 93d72b2 commit 439cf3b

2 files changed

Lines changed: 4 additions & 0 deletions

File tree

verification/proofs/idris2/AxiomPolicyOrdering.idr

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@
2121

2222
module AxiomPolicyOrdering
2323

24+
import Data.Nat
25+
2426
%default total
2527

2628
-- ==========================================================================

verification/proofs/idris2/TrustLevelSoundness.idr

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@
2020

2121
module TrustLevelSoundness
2222

23+
import Data.Nat
24+
2325
%default total
2426

2527
-- ==========================================================================

0 commit comments

Comments
 (0)