def
Lean.Elab.WF.elabWFRel
(preDefs : Array Lean.Elab.PreDefinition)
(unaryPreDef : Lean.Elab.PreDefinition)
(wf? : Option Lean.Elab.WF.TerminationWF)
:
Equations
- Lean.Elab.WF.elabWFRel preDefs unaryPreDef wf? = let α := Lean.Expr.bindingDomain! unaryPreDef.type; do let u ← liftM (Lean.Meta.getLevel α) let expectedType : Lean.Expr := Lean.mkApp (Lean.mkConst `WellFoundedRelation [u]) α match wf? with | some (Lean.Elab.WF.TerminationWF.core wfStx) => Lean.Elab.Term.withDeclName unaryPreDef.declName do let a ← Lean.Elab.Term.withSynthesize (Lean.Elab.Term.elabTermEnsuringType wfStx (some expectedType) true true none) let wfRel ← liftM (Lean.Meta.instantiateMVars a) let pendingMVarIds ← liftM (Lean.Meta.getMVars wfRel) discard (Lean.Elab.Term.logUnassignedUsingErrorInfos pendingMVarIds none) pure wfRel | some (Lean.Elab.WF.TerminationWF.ext elements) => Lean.Elab.Term.withDeclName unaryPreDef.declName (Lean.withRef (Lean.Elab.WF.getRefFromElems elements) do let a ← liftM (Lean.Meta.mkFreshExprSyntheticOpaqueMVar expectedType Lean.Name.anonymous) let mainMVarId : Lean.MVarId := Lean.Expr.mvarId! a let a ← liftM (Lean.Meta.mkConstWithFreshMVarLevels `invImage) let discr ← liftM (Lean.Meta.apply mainMVarId a) match discr with | [fMVarId, wfRelMVarId, x] => do let discr ← liftM (Lean.Meta.intro1 fMVarId) let x : Lean.FVarId × Lean.MVarId := discr match x with | (d, fMVarId) => do let subgoals ← Lean.Elab.WF.unpackMutual preDefs fMVarId d let s : Subarray Lean.Elab.WF.TerminationByElement := toStream elements let s_1 : Subarray Lean.Elab.PreDefinition := toStream preDefs let r ← forIn subgoals { fst := s, snd := s_1 } fun x r => match x with | (d, mvarId) => let s := r.fst; let s_2 := r.snd; match Stream.next? s_2 with | none => pure (ForInStep.done { fst := s, snd := s_2 }) | some (preDef, s') => let s_3 := s'; match Stream.next? s with | none => pure (ForInStep.done { fst := s, snd := s_3 }) | some (element, s') => let s := s'; do let mvarId ← Lean.Elab.WF.unpackUnary preDef mvarId d element Lean.Meta.withMVarContext mvarId do let a ← liftM (Lean.Meta.getMVarType mvarId) let value ← Lean.Elab.Term.withSynthesize (Lean.Elab.Term.elabTermEnsuringType element.body (some a) true true none) liftM (Lean.Meta.assignExprMVar mvarId value) pure (ForInStep.yield { fst := s, snd := s_3 }) let x : MProd (Subarray Lean.Elab.WF.TerminationByElement) (Subarray Lean.Elab.PreDefinition) := r match x with | { fst := s, snd := s_2 } => do let a ← liftM (Lean.Meta.inferType (Lean.mkMVar wfRelMVarId)) let wfRelVal ← liftM (Lean.Meta.synthInstance a none) liftM (Lean.Meta.assignExprMVar wfRelMVarId wfRelVal) liftM (Lean.Meta.instantiateMVars (Lean.mkMVar mainMVarId)) | x => Lean.throwError (Lean.toMessageData "failed to apply 'invImage'")) | none => Lean.throwError (Lean.toMessageData "'termination_by' modifier missing")