law maybe_map_id_sym

bend-mathlib@0.8.1.0 · maybe.bend:282

import Base

282# Mapping the identity gives the value back, reversed to rewrite toward the simple side.
283law maybe_map_id_sym:
284  for ~A: Data
285  for m: Maybe<&2, A>
286  {m == Maybe.map(&2, A, A, x => x, m) : Maybe<&2, A>}