meta theory

Stream: general

[Johan Commelin]

noncomputable theory

-- the rest of this file doesn't need the `noncomputable` keyword (modulo caveats)

Is there an equivalent

meta theory -- make all the defs in this file `meta`

[Johan Commelin]

Actually, can I create a new command mdef that does meta def? (I'll change mdef to laat locally. Which is the dutch word for "let".)
I want someone to play with lean without bothering about well-founded recursion.

[Johan Commelin]

Is this even possible in Lean 3, or should I use Lean 4 for this?

[Mario Carneiro]

it's not implemented in lean 3, but it might be possible to do