Generate the correct list hook implementation

runtimeverification · Jan 21, 2025 · d8545f5 · d8545f5
1 parent 61c7f7e
commit d8545f5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py
@@ -150,7 +150,7 @@ def _collection(self, sort: str) -> Structure:
         match coll.kind:
             case CollectionKind.LIST:
                 (item,) = sorts
-                val = Term(f'List {item}')
+                val = Term(f'(ListHook {item}).list')
             case CollectionKind.SET:
                 (item,) = sorts
                 val = Term(f'(SetHook {item}).set')