From 60832d1ec7854aceba43fe6511eef2cef27a6485 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 22 Jan 2025 15:51:31 +0000 Subject: [PATCH] Fix prelude --- 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 d8b5de0e97..a7d4e04c63 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -20,7 +20,7 @@ These theorems should be provable directly from the function rules and the seman -/ -- Basic K types -abbrev SortBool : Type := Int +abbrev SortBool : Type := Bool abbrev SortBytes : Type := ByteArray abbrev SortId : Type := String abbrev SortInt : Type := Int