0

I'm running through logic foundations and during the lower_grade_lowers exercise, Coq is behaving in a way that I wouldn't expect.

I have the following goal:

  grade_comparison match l with
                   | A | _ => Grade l Natural
                   end (Grade l Plus) = Lt

This, to me, feels like it should simplify: the | A | _ => ... branch is not falsifiable, and I would expect Coq to simplify the whole thing to:

grade_comparison (Grade l Natural) (Grade l Plus) = Lt

This does not happen, and I do not understand why...

1
  • Maybe because Grade l Natural is guarded behind a match; did you try running destruct l. at this point?
    – ErikMD
    Sep 3 at 23:02

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.