Skip to content

I
Iris
Commit dcd54605 authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

Make coqchk slightly happier with prelude/pretty 

Unfortunately, it still fails in iris.prelude.pretty.pretty_N_inj
parent 3c60ccc3
Pipeline #2604 passed with stage
    in 4 minutes and 14 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 2 additions and 1 deletion
    prelude/pretty.v
    View file @ dcd54605
    ......@@ -32,7 +32,8 @@ Lemma pretty_N_go_step x s :
    = pretty_N_go (x `div` 10) (String (pretty_N_char (x `mod` 10)) s).
    Proof.
    unfold pretty_N_go; intros; destruct (wf_guard 32 N.lt_wf_0 x).
    unfold pretty_N_go_help; fold pretty_N_go_help.
    destruct wf_guard. (* this makes coqchk happy. *)
    unfold pretty_N_go_help at 1; fold pretty_N_go_help.
    by destruct (decide (0 < x)%N); auto using pretty_N_go_help_irrel.
    Qed.
    Instance pretty_N : Pretty N := λ x, pretty_N_go x ""%string.
    ......
    Markdown is supported
    0% or
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment