law maybe_map_id

bend-mathlib@0.8.1.0 · maybe.bend:73

import Base

73# Mapping the identity gives the value back.
74law maybe_map_id:
75  for ~A: Data
76  for m: Maybe<&2, A>
77  {Maybe.map(&2, A, A, x => x, m) == m : Maybe<&2, A>}