Open sweirich opened 6 years ago
Right now axiomatize module has the potential to introduce inconsistent axioms.
We could fix this by using default instead. I.e. instead of generating
Axiom mkFoo : Int -> Char -> Foo.
we could generate
Definition mkFoo : Int -> Char -> Foo := GHC.Err.default.
as long as we have a default value for type Foo.
Foo
If we go forward with this strategy, we should make default instance definition more automatic. But should do that already.
Right now axiomatize module has the potential to introduce inconsistent axioms.
We could fix this by using default instead. I.e. instead of generating
we could generate
as long as we have a default value for type
Foo.If we go forward with this strategy, we should make default instance definition more automatic. But should do that already.