RedPRL/sml-redprl

Bug in HCom.Eq

Closed this issue · 2 comments

jonsterling commented

While documenting our rules, @timjb noticed that the HCom.Eq rule does not seem to be checking that the type arguments of the two compositions are equal. This seems wrong to me, but I might be confused...

@favonia Do we need to change the subgoal?

favonia commented

Yes. It is a bug introduced in cd276c0 in PR #502 (sorry) and should be fixed.

  • 👍1
jonsterling commented

@favonia OK! I think it's easy to fix.