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

Merged
aniva merged 1 commits from repl/elab-option into dev 2025-05-01 09:00:04 -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.
aniva added this to the 0.3.1 milestone 2025-04-10 23:19:57 -07:00
aniva added the
part/REPL
part/Elab
category
feature
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
aniva merged commit 0a987174bc into dev 2025-05-01 09:00:04 -07:00
Sign in to join this conversation.
No description provided.