From 4f8646e3be43fcfa46f34bfa45f7560d32f71da5 Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Thu, 16 Jan 2025 13:14:48 +0100 Subject: [PATCH] Better writing of `nodupAx` --- pyk/src/pyk/k2lean4/Prelude.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index 31196456e7f..f5bdca6b661 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -78,7 +78,7 @@ axiom valuesAx : mapCAx → List V axiom sizeAx : mapCAx → Nat axiom includesAx : mapCAx → mapCAx → Bool -- map inclusion axiom choiceAx : mapCAx → K -- arbitrary key from a map -axiom nodupAx : forall al : mapCAx, List.Nodup (keysAx K al) +axiom nodupAx : forall m, List.Nodup (keysAx K m) -- Uninterpreted Map implementation noncomputable def mapImpl (K V : Type) : MapHookSig K V :=