fix(repl): Elaborate with errToSorry as false by default #187

aniva · 2025-04-10T23:19:57-07:00

aniva commented

2025-04-10 23:19:57 -07:00

We address two cases. One is ambiguous elaboration. For example if exp is a type class function that can act on both Nat and Real

example : exp 2 <= exp 3

The other case is we don't collect goals with sorrys in them. For example,

example : f true = f false

with f being undefined. The old behaviour would emit a goal with sorry in its target type and this is pathological.

We address two cases. One is ambiguous elaboration. For example if `exp` is a type class function that can act on both `Nat` and `Real` ``` example : exp 2 <= exp 3 ``` The other case is we don't collect goals with `sorry`s in them. For example, ``` example : f true = f false ``` with `f` being undefined. The old behaviour would emit a goal with `sorry` in its target type and this is pathological.

aniva added this to the 0.3.1 milestone 2025-04-10 23:19:57 -07:00

aniva added the

labels 2025-04-10 23:19:57 -07:00

aniva self-assigned this 2025-04-10 23:19:57 -07:00

aniva added 1 commit 2025-04-10 23:19:57 -07:00

14b74b612d

fix(repl): Elaborate with `errToSorry` as false by default

This pull request can be merged automatically.