Theory ML_Lenses

✐‹creator "Kevin Kappelmann"›
section ‹Lenses›
theory ML_Lenses
  imports
    ML_ICategories
begin

ML_gen_file‹lens.ML›

(*standard function space lense*)
ML‹
structure \<^eval>‹sfx_ParaT_nargs "SLens"› =
\<^eval>‹sfx_ParaT_nargs "Lens"›(
  structure L = \<^eval>‹sfx_ParaT_nargs "Lens_Base"›(
    \<^eval>‹sfx_ParaT_nargs "Arrow_Apply"›(
      \<^eval>‹sfx_ParaT_nargs "SArrow_Apply"›))
  structure A = \<^eval>‹sfx_ParaT_nargs "Arrow"›(\<^eval>‹sfx_ParaT_nargs "SArrow_Apply"›))

signature \<^eval>‹sfx_ParaT_nargs "SLENS"› =
  \<^eval>‹sfx_ParaT_nargs "LENS"›
  where type (@{ParaT_args} 'a, 'b) C.morph = 'a -> 'b
  where type (@{ParaT_args} 't, 'o, 's, 'i) lens =
    (@{ParaT_args} 't, 'o, 's, 'i) \<^eval>‹sfx_ParaT_nargs "SLens" ^ ".lens"›
›

end