Documentation

Lean.Elab.PreDefinition.Structural.IndGroupInfo

This module contains the types

One purpose of this abstraction is to make it clear when a fuction operates on a group as a whole, rather than a specific inductive within the group.

A mutually inductive group, identified by the all array of the InductiveVal of its constituents.

Instances For
    Equations
    • group.numMotives = group.all.size + group.numNested
    Instances For

      Instantiates the right .brecOn or .bInductionOn for the given type former index, including universe parameters and fixed prefix.

      An instance of an mutually inductive group of inductives, identified by the all array and the level and expressions parameters.

      For example this distinguishes between List α and List β so that we will not even attempt mutual structural recursion on such incompatible types.

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

          Instantiates the right .brecOn or .bInductionOn for the given type former index, including universe parameters and fixed prefix.

          Equations
          • group.brecOn ind lvl idx = let n := group.brecOnName ind idx; let us := if ind = true then group.levels else lvl :: group.levels; Lean.mkAppN (Lean.Expr.const n us) group.params
          Instances For

            Figures out the nested type formers of an inductive group, with parameters instantiated and indices still forall-abstracted.

            For example given a nested inductive

            inductive Tree α where | node : α → Vector (Tree α) n → Tree α
            

            (where n is an index of Vector) and the instantiation Tree Int it will return

            #[(n : Nat) → Vector (Tree Int) n]
            
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For