agda2hs icon indicating copy to clipboard operation
agda2hs copied to clipboard

Published 20 hours ago • verified publisher icon agda

[ fix #302 ] Move _/=_ function out of the Eq record

Open jespercockx opened this issue 10 months ago • 1 comments

jespercockx avatar Apr 12 '24 12:04 jespercockx

@jespercockx The golden file is missing; feel free to cherry-pick the fix from the issue302-fix branch: https://github.com/agda/agda2hs/commit/a9d79b81299e4ea245634b561f1b7e320d67aa83

omelkonian avatar Apr 19 '24 11:04 omelkonian

If we want to stay faithful to the Haskell interface, shouldn't _/= _ be turned into a record field instead?

flupe avatar May 22 '24 08:05 flupe

If we want to stay faithful to the Haskell interface, shouldn't _/= _ be turned into a record field instead?

Ideally yes, but (1) it would break current code and (2) there seem to be some plans to move (/=) out of the type class in the Haskell prelude.

jespercockx avatar May 24 '24 12:05 jespercockx