skip constructor

[sweirich]

When I skip all except for the NoUnfolding constructor of the Unfolding data type, hs-to-coq produces the wrong output for this input.

hasSomeUnfolding :: Unfolding -> Bool
hasSomeUnfolding NoUnfolding   = False
hasSomeUnfolding BootUnfolding = False
hasSomeUnfolding _             = True

Specifically, the result is:

Definition hasSomeUnfolding : Unfolding -> bool :=
  fun arg_0__ => match arg_0__ with | NoUnfolding => false | _ => true end.

which Coq rejects because of the redundant pattern.

I'm currently working around by skipping this function.

[antalsz]

Ah, the expected edge cases. This may be tricky to eliminate algorithmically – would a

skip equation Core.hasSomeUnfolding _

edit work instead? That might be simpler.

[antalsz]

8180fd5 adds the aforementioned skip equation edit, which was much simpler to add than a pattern redundancy checker. I'm closing this, but I've created #135 to remind us to consider adding automatic redundancy checking.