Stream: General

Topic: Sepref implemntation Binding

view this post on Zulip Valentin Springsklee (Jan 27 2023 at 15:14):

Hello, I want to bind a HOL function to an imperative HOL function using the sepref_decl_impl keyword. I want to represent a HOL nat set as a HashSet (hs.assn nat assn). When I want to proof the sepref_decl_impl, I get no subgoal, but cannot close the goal due to the error: "chk_result: Invalid pattern left in assertions: hr_comp (hs.assn nat_assn) (⟨nat_rel⟩set_rel)". Can any give me any insight how to avoid this error during refinement? It is generated in the theory Sepref_Rules.

view this post on Zulip Valentin Springsklee (Jan 27 2023 at 15:32):

OK, never mind, I figured it out!

Last updated: Dec 30 2024 at 16:22 UTC