Skip to content

Set `simpl never` for `Pos` and `N`.

Robbert Krebbers requested to merge robbert/simpl_never_pos_n into master

Previously, we set simpl never for just Pos.mul and N.add. That's pretty inconsistent and annoying. For example:

Eval simpl in (2 + x)%positive.
(*
     = match x with
       | q~1 => match q with
                | q0~1 => (Pos.succ q0)~0
                | q0~0 => q0~1
                | 1 => 2
                end~1
       | q~0 => match q with
                | q0~1 => (Pos.succ q0)~0
                | q0~0 => q0~1
                | 1 => 2
                end~0
       | 1 => 3
       end
     : positive
*)

I copied the list of simpl never declarations for Z and removed the operations (e.g., opp) that are not available for N or Pos.

Edited by Robbert Krebbers

Merge request reports

Loading