| import Lean | |
| axiom ex (p q : Prop) (h : p ∧ q) : q ∧ q | |
| open Lean in | |
| open Lean.Meta in | |
| def test : MetaM Unit := do | |
| let type := (← getConstInfo ``ex).type | |
| let mvar ← mkFreshExprMVar type | |
| let (#[p, q, h], mvarId) ← mvar.mvarId!.introNP 3 | throwError "unexpected" | |
| trace[Meta.debug] "{MessageData.ofGoal mvarId}" | |
| let (s₁, s₂) ← mvarId.byCases (mkFVar p) `hAux | |
| trace[Meta.debug] "{MessageData.ofGoal s₁.mvarId}\n------\n{MessageData.ofGoal s₂.mvarId}" | |
| return () | |
| set_option trace.Meta.debug true | |
| #eval test |