Theory Fofu_Impl_Base

theory Fofu_Impl_Base
imports CAVA_Base Array_List Rewrite Refine_Monadic_Syntax_Sugar
theory Fofu_Impl_Base
imports 
  CAVA_Base 
  "cava/Libs/Refine_Imperative_HOL/Sepref"
  "cava/Libs/Refine_Imperative_HOL/Heaps/Array_List"
  "~~/src/HOL/Library/Rewrite"
  Refine_Monadic_Syntax_Sugar
begin
  hide_type (open) List_Seg.node

  interpretation Refine_Monadic_Syntax .


end