Open JLimperg opened 6 days ago
The issue here is that Exception.internal
has a default argument.
inductive Exception where
| error (ref : Syntax) (msg : MessageData)
| internal (id : InternalExceptionId) (extra : KVMap := {})
Thus, .internal ..
is equivalent to .internal _ {}
. Possible solutions:
..
. Workaround.
import Lean
open Lean
example (e : Exception) : True :=
match e with
| .internal _ _ => sorry
| .error .. => sorry
Ah, it's the default argument! I understand ..
as "ignore all other arguments", so I would prefer if there was no distinction between arguments with and without a default value.
Prerequisites
Please put an X between the brackets as you perform the following steps:
Description
MWE:
Versions
"4.10.0-nightly-2024-06-24"
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.