Documentation

Batteries.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
    Instances For

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

      Equations
        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
            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
                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
                        Instances For

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

                          Equations
                            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
                                Instances For

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

                                  Equations
                                    Instances For

                                      Finds the TermInfo for an elaborated term stx.

                                      Equations
                                        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
                                            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
                                                    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