Documentation

Lean.Meta.Tactic.Util

Get the user name of the given metavariable.

Equations
  • mvarId.getTag = do let __do_liftmvarId.getDecl pure __do_lift.userName
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      Instances For
        Equations
        Instances For
          def Lean.Meta.throwTacticEx {α : Type} (tacticName : Lake.Name) (mvarId : Lean.MVarId) (msg? : optParam (Option Lean.MessageData) none) :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Throw a tactic exception with given tactic name if the given metavariable is assigned.

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

                Get the type the given metavariable.

                Equations
                • mvarId.getType = do let __do_liftmvarId.getDecl pure __do_lift.type
                Instances For

                  Get the type the given metavariable after instantiating metavariables and reducing to weak head normal form.

                  Equations
                  Instances For

                    Assign mvarId to sorryAx

                    Equations
                    • mvarId.admit synthetic = mvarId.withContext do mvarId.checkNotAssigned `admit let mvarTypemvarId.getType let valLean.Meta.mkSorry mvarType synthetic mvarId.assign val
                    Instances For

                      Beta reduce the metavariable type head

                      Equations
                      • mvarId.headBetaType = do let __do_liftmvarId.getType mvarId.setType __do_lift.headBeta
                      Instances For

                        Collect nondependent hypotheses that are propositions.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          Instances For
                            def Lean.Meta.exactlyOne (mvarIds : List Lean.MVarId) (msg : optParam Lean.MessageData ((Lean.MessageData.ofFormat Std.format) "unexpected number of goals")) :
                            Equations
                            Instances For
                              def Lean.Meta.ensureAtMostOne (mvarIds : List Lean.MVarId) (msg : optParam Lean.MessageData ((Lean.MessageData.ofFormat Std.format) "unexpected number of goals")) :
                              Equations
                              Instances For

                                Return all propositions in the local context.

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

                                    Check if a goal is of a subsingleton type.

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