Theory ML_Structured_Lenses

✐‹creator "Kevin Kappelmann"›
section ‹Structured Lenses›
theory ML_Structured_Lenses
  imports
    ML_Gen_Zippers_Setup
begin

ML_gen_file‹structured_lens.ML›
ML_gen_file‹sstructured_lens.ML›
ML_gen_file‹comp_structured_lens.ML›
ML_gen_file‹modify_structured_lens.ML›
ML_gen_file‹pair_structured_lens.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 files, just with different parameters.›
ML_gen_file‹structured_lens.ML›
ML_gen_file‹sstructured_lens.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›

end