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

Merged

aniva merged 1 commit from repl/elab-option into dev

2025-05-01 09:00:04 -07:00

aniva commented

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

Owner

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.