From 22f2edabc5e8242a3184c58967fbb48ce6e69952 Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Tue, 21 Jan 2025 16:01:20 +0100 Subject: [PATCH] Remove `Option` type for `total` functions --- pyk/src/pyk/k2lean4/k2lean4.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index 194e81b416..f40ed87e90 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/pyk/src/pyk/k2lean4/k2lean4.py @@ -219,12 +219,13 @@ def _transform_func(self, func: str) -> Axiom: sort_params = [var.name for var in decl.symbol.vars] param_sorts = [sort.name for sort in decl.param_sorts] sort = decl.sort.name + option_type = '' if 'total' in decl.attrs_by_key else 'Option ' binders: list[Binder] = [] if sort_params: binders.append(ImplBinder(sort_params, Term('Type'))) binders.extend(ExplBinder((f'x{i}',), Term(sort)) for i, sort in enumerate(param_sorts)) - return Axiom(ident, Signature(binders, Term(f'Option {sort}'))) + return Axiom(ident, Signature(binders, Term(f'{option_type}{sort}'))) def _param_sorts(decl: SymbolDecl) -> list[str]: