strange internal exception

Stream: lean4

[Koundinya Vajjha]

The following throws an internal exception #3 for some reason:

prelude

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

theorem Or.elim {c : Prop} (h : Or a b) (left : a → c)
  (right : b → c) : c := sorry -- internal exception #3

Any help on what is happening here? For more context, I'm trying to create a self-contained lean file that does not rely on the prelude and demonstrates iota reduction (pattern matching) in a proof.

[Paul Reichert]

I tried pasting the content of Init.Prelude into Lean4Web, adding your code (renamed to Or') at the end and mimimizing it. I don't know for sure, but probably the elaborator for theorems somewhere relies on the Name structure being in the environment. You shouldn't expect everything to work normally without importing Init.Prelude. Many tactics, such as omega, even rely on having imported Init.

Can't you just import Init and use a different name, such as Or', to prevent the name clash?

[Joachim Breitner]

Also note that use of prelude outside of the official prelude is not officially supported. You are welcome to play around with it, but issues you find may not be fixed.

If you just want to #mwe an issue to report to the Lean repo, it suffices to make sure it doesn't depend on Mathlib.

[François G. Dorais]

You need a few basic defs from Init.Prelude for lean to work properly, so this works:

prelude
import Init.Prelude

namespace My

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

theorem Or.elim {c : Prop} (h : Or a b) (left : a → c)
  (right : b → c) : c := sorry