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

    Auxiliary type for synthesizeSyntheticMVars. It specifies whether pending synthetic metavariables can be postponed or not.

    • yes: Lean.Elab.Term.PostponeBehavior

      Any kind of pending synthetic metavariable can be postponed. Universe constrains may also be postponed.

    • no: Lean.Elab.Term.PostponeBehavior

      Pending synthetic metavariables cannot be postponed.

    • partial: Lean.Elab.Term.PostponeBehavior

      Synthectic metavariables associated with type class resolution can be postponed. Motivation: this kind of metavariable are not synthetic opaque, and can be assigned by isDefEq. Unviverse constraints can also be postponed.

    Instances For

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

      The tacticCode syntax comprises the whole by ... expression.

      If report := false, then runTactic will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions.

      Try to process pending synthetic metavariables.

      If postpone == .no,then pendingMVars is [] after executing this method. If postpone == .partial, then pendingMVars contains only .tc and .coe kinds.

      It keeps executing synthesizeSyntheticMVarsStep while progress is being made. If postpone != .yes, then it applies default instances to SyntheticMVarKind.typeClass (if available) metavariables that are still unresolved, and then tries to resolve metavariables with postponeOnError == 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 If postpone == .no.

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

      @[inline]

      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]

        Similar to withSynthesize, but uses postpone := .true, does 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