Skip to content

set_solver does not unfold is_Some

Example foo : is_Some (({[ 10 := 55 ]} : gmap nat nat) !! 10).
Proof.
  Fail set_solver. (* No matching clauses for match. *)
  unfold is_Some. set_solver. (* Works. *)
Qed.