Theory ML_Alternating_Zipper_Nodes

✐‹creator "Kevin Kappelmann"›
theory ML_Alternating_Zipper_Nodes
  imports
    ML_Alternating_Zippers
begin

ML_gen_file‹node.ML›
ML_gen_file‹modify_node_content.ML›
ML_gen_file‹modify_node_next.ML›

setup‹fn theory =>
let val nzippers = ML_Gen.nzippers () + 1
in Context.theory_map (ML_Gen.setup_zipper_args' (NONE, NONE) (SOME nzippers, NONE)) theory end›
text ‹Note: we reload the ML file @{file node.ML}, just with different parameters.›
ML_gen_file‹node.ML›
ML‹
  val succ_node_sig = sfx_T_nargs "NODE"
  val succ_node_functor = sfx_T_nargs "Node"
›
setup‹fn theory =>
let val nzippers = ML_Gen.nzippers () - 1
in Context.theory_map (ML_Gen.setup_zipper_args' (NONE, NONE) (SOME nzippers, NONE)) theory end›

context
  notes [[imap stop: ‹ML_Gen.nzippers () + 1›]]
begin
ML_gen_file‹instantiate_node_succ.ML›
end

ML_gen_file‹alternating_zipper_nodes.ML›
ML_gen_file‹alternating_zipper_nodes_zippers.ML›
ML_gen_file‹alternating_zipper_nodes_simple_zippers.ML›

end