diff --git a/pyk/src/pyk/k2lean4/model.py b/pyk/src/pyk/k2lean4/model.py index 0a09fb699d..39e763e801 100644 --- a/pyk/src/pyk/k2lean4/model.py +++ b/pyk/src/pyk/k2lean4/model.py @@ -136,6 +136,8 @@ def __init__( ident: str | DeclId | None = None, modifiers: Modifiers | None = None, ): + if priority and priority < 0: + raise ValueError('Priority must be non-negative') if not signature.ty: # TODO refine type to avoid this check raise ValueError('Missing type from signature')