Documentation

Lean.Elab.SyntheticMVars

We use this method to report typeclass (and coercion) resolution problems that are "stuck". That is, there is nothing else to do, and we don't have enough information to synthesize them using TC resolution.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Try to synthesize a term val using the tactic code tacticCode, and then assign mvarId := val.

    Try to process pending synthetic metavariables. If mayPostpone == false, then pendingMVars is [] after executing this method.

    It keeps executing synthesizeSyntheticMVarsStep while progress is being made. If mayPostpone == false, then it applies default instances to SyntheticMVarKind.typeClass (if available) metavariables that are still unresolved, and then tries to resolve metavariables with mayPostpone == false. That is, we force them to produce error messages and/or commit to a "best option". If, after that, we still haven't made progress, we report "stuck" errors.

    Remark: we set ignoreStuckTC := true when elaborating simp arguments. Then, pending TC problems become implicit parameters for the simp theorem.

    @[inline]
    def Lean.Elab.Term.withSynthesize {m : TypeType u_1} {α : Type} [MonadFunctorT Lean.Elab.TermElabM m] [Monad m] (k : m α) (mayPostpone : optParam Bool false) :
    m α

    Execute k, and synthesize pending synthetic metavariables created while executing k are solved. If mayPostpone == false, then all of them must be synthesized. Remark: even if mayPostpone == true, the method still uses synthesizeUsingDefault

    Equations
    Instances For
      @[inline]
      def Lean.Elab.Term.withSynthesizeLight {m : TypeType u_1} {α : Type} [MonadFunctorT Lean.Elab.TermElabM m] [Monad m] (k : m α) :
      m α

      Similar to withSynthesize, but sets mayPostpone to true, and do not use synthesizeUsingDefault

      Equations
      Instances For

        Elaborate stx, and make sure all pending synthetic metavariables created while elaborating stx are solved.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Collect unassigned metavariables at e that have associated tactic blocks, and then execute them using runTactic. We use this method at the match .. with elaborator when it cannot be postponed anymore, but it is still waiting the result of a tactic block.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For