From 1ffb4659608e3a211a43b44fd816824563a912e2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 16 Jan 2025 13:56:52 +0000 Subject: [PATCH] Enforce `priority` to be non-negative --- pyk/src/pyk/k2lean4/model.py | 2 ++ 1 file changed, 2 insertions(+) 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')