Documentation

Std.CodeAction.Misc

Miscellaneous code actions #

This declares some basic tactic code actions, using the @[tactic_code_action] API.

Return the syntax stack leading to target from root, if one exists.

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

    Constructs a hole with a kind matching the provided hole elaborator.

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

      Hole code action used to fill in a structure's field when specifying an instance.

      In the following:

      instance : Monad Id := _
      

      invoking the hole code action "Generate a (minimal) skeleton for the structure under construction." produces:

      instance : Monad Id where
        pure := _
        bind := _
      

      and invoking "Generate a (maximal) skeleton for the structure under construction." produces:

      instance : Monad Id where
        map := _
        mapConst := _
        pure := _
        seq := _
        seqLeft := _
        seqRight := _
        bind := _
      
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Returns true if this field is an autoParam or optParam, or if it is given an optional value in a child struct.

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

          Returns the fields of a structure, unfolding parent structures.

          Returns the explicit arguments given a type.

          Equations
          Instances For

            Invoking hole code action "Generate a list of equations for a recursive definition" in the following:

            def foo : Expr → Unit := _
            

            produces:

            def foo : Expr → Unit := fun
              | .bvar deBruijnIndex => _
              | .fvar fvarId => _
              | .mvar mvarId => _
              | .sort u => _
              | .const declName us => _
              | .app fn arg => _
              | .lam binderName binderType body binderInfo => _
              | .forallE binderName binderType body binderInfo => _
              | .letE declName type value body nonDep => _
              | .lit _ => _
              | .mdata data expr => _
              | .proj typeName idx struct => _
            
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Invoking hole code action "Start a tactic proof" will fill in a hole with by done.

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

                The "Remove tactics after 'no goals'" code action deletes any tactics following a completed proof.

                example : True := by
                  trivial
                  trivial -- <- remove this, proof is already done
                  rfl
                

                is transformed to

                example : True := by
                  trivial
                
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Similar to getElabInfo, but returns the names of binders instead of just the numbers; intended for code actions which need to name the binders.

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

                    Invoking tactic code action "Generate an explicit pattern match for 'induction'" in the following:

                    example (x : Nat) : x = x := by
                      induction x
                    

                    produces:

                    example (x : Nat) : x = x := by
                      induction x with
                      | zero => sorry
                      | succ n ih => sorry
                    

                    It also works for cases.

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

                      The "Add subgoals" code action puts · done subgoals for any goals remaining at the end of a proof.

                      example : TrueTrue := by
                        constructor
                        -- <- here
                      

                      is transformed to

                      example : TrueTrue := by
                        constructor
                        · done
                        · done
                      
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        The "Add subgoals" code action puts · done subgoals for any goals remaining at the end of a proof.

                        example : TrueTrue := by
                          constructor
                          -- <- here
                        

                        is transformed to

                        example : TrueTrue := by
                          constructor
                          · done
                          · done
                        
                        Equations
                        Instances For

                          The "Add subgoals" code action puts · done subgoals for any goals remaining at the end of a proof.

                          example : TrueTrue := by
                            constructor
                            -- <- here
                          

                          is transformed to

                          example : TrueTrue := by
                            constructor
                            · done
                            · done
                          
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For