Documentation

Lean.Declaration

Reducibility hints are used in the convertibility checker. When trying to solve a constraint such a

       (f ...) =?= (g ...)

where f and g are definitions, the checker has to decide which one will be unfolded. If f (g) is opaque, then g (f) is unfolded if it is also not marked as opaque, Else if f (g) is abbrev, then f (g) is unfolded if g (f) is also not marked as abbrev, Else if f and g are regular, then we unfold the one with the biggest definitional height. Otherwise both are unfolded.

The arguments of the regular Constructor are: the definitional height and the flag selfOpt.

The definitional height is by default computed by the kernel. It only takes into account other regular definitions used in a definition. When creating declarations using meta-programming, we can specify the definitional depth manually.

Remark: the hint only affects performance. None of the hints prevent the kernel from unfolding a declaration during Type checking.

Remark: the ReducibilityHints are not related to the attributes: reducible/irrelevance/semireducible. These attributes are used by the Elaborator. The ReducibilityHints are used by the kernel (and Elaborator). Moreover, the ReducibilityHints cannot be changed after a declaration is added to the kernel.

Instances For
    @[export lean_reducibility_hints_get_height]
    Equations
    Instances For
      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
          Equations
          Instances For
            Equations
            Instances For

              Base structure for AxiomVal, DefinitionVal, TheoremVal, InductiveVal, ConstructorVal, RecursorVal and QuotVal.

              Instances For
                Equations
                Instances For
                  Equations
                  @[export lean_mk_axiom_val]
                  def Lean.mkAxiomValEx (name : Lake.Name) (levelParams : List Lake.Name) (type : Lean.Expr) (isUnsafe : Bool) :
                  Equations
                  • Lean.mkAxiomValEx name levelParams type isUnsafe = { name := name, levelParams := levelParams, type := type, isUnsafe := isUnsafe }
                  Instances For
                    @[export lean_axiom_val_is_unsafe]
                    Equations
                    • v.isUnsafeEx = v.isUnsafe
                    Instances For
                      Instances For
                        Equations
                        @[export lean_mk_definition_val]
                        Equations
                        • Lean.mkDefinitionValEx name levelParams type value hints safety all = { name := name, levelParams := levelParams, type := type, value := value, hints := hints, safety := safety, all := all }
                        Instances For
                          @[export lean_definition_val_get_safety]
                          Equations
                          • v.getSafetyEx = v.safety
                          Instances For
                            Instances For
                              Equations
                              @[export lean_mk_theorem_val]
                              def Lean.mkTheoremValEx (name : Lake.Name) (levelParams : List Lake.Name) (type : Lean.Expr) (value : Lean.Expr) (all : List Lake.Name) :
                              Equations
                              • Lean.mkTheoremValEx name levelParams type value all = { name := name, levelParams := levelParams, type := type, value := value, all := all }
                              Instances For

                                Value for an opaque constant declaration opaque x : t := e

                                Instances For
                                  Equations
                                  @[export lean_mk_opaque_val]
                                  def Lean.mkOpaqueValEx (name : Lake.Name) (levelParams : List Lake.Name) (type : Lean.Expr) (value : Lean.Expr) (isUnsafe : Bool) (all : List Lake.Name) :
                                  Equations
                                  • Lean.mkOpaqueValEx name levelParams type value isUnsafe all = { name := name, levelParams := levelParams, type := type, value := value, isUnsafe := isUnsafe, all := all }
                                  Instances For
                                    @[export lean_opaque_val_is_unsafe]
                                    Equations
                                    • v.isUnsafeEx = v.isUnsafe
                                    Instances For
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations

                                          Declaration object that can be sent to the kernel.

                                          Instances For
                                            @[export lean_mk_inductive_decl]
                                            def Lean.mkInductiveDeclEs (lparams : List Lake.Name) (nparams : Nat) (types : List Lean.InductiveType) (isUnsafe : Bool) :
                                            Equations
                                            Instances For
                                              @[export lean_is_unsafe_inductive_decl]
                                              Equations
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[specialize #[]]
                                                  def Lean.Declaration.foldExprM {α : Type} {m : TypeType} [Monad m] (d : Lean.Declaration) (f : αLean.Exprm α) (a : α) :
                                                  m α
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[inline]
                                                    Equations
                                                    Instances For

                                                      The kernel compiles (mutual) inductive declarations (see inductiveDecls) into a set of

                                                      • Declaration.inductDecl (for each inductive datatype in the mutual Declaration),
                                                      • Declaration.ctorDecl (for each Constructor in the mutual Declaration),
                                                      • Declaration.recDecl (automatically generated recursors).

                                                      This data is used to implement iota-reduction efficiently and compile nested inductive declarations.

                                                      A series of checks are performed by the kernel to check whether a inductiveDecls is valid or not.

                                                      • name : Lake.Name
                                                      • levelParams : List Lake.Name
                                                      • type : Lean.Expr
                                                      • numParams : Nat

                                                        Number of parameters. A parameter is an argument to the defined type that is fixed over constructors. An example of this is the α : Type argument in the vector constructors nil : Vector α 0 and cons : α → Vector α n → Vector α (n+1).

                                                        The intuition is that the inductive type must exhibit parametric polymorphism over the inductive parameter, as opposed to ad-hoc polymorphism.

                                                      • numIndices : Nat

                                                        Number of indices. An index is an argument that varies over constructors.

                                                        An example of this is the n : Nat argument in the vector constructor cons : α → Vector α n → Vector α (n+1).

                                                      • List of all (including this one) inductive datatypes in the mutual declaration containing this one

                                                      • ctors : List Lake.Name

                                                        List of the names of the constructors for this inductive datatype.

                                                      • isRec : Bool

                                                        true when recursive (that is, the inductive type appears as an argument in a constructor).

                                                      • isUnsafe : Bool

                                                        Whether the definition is flagged as unsafe.

                                                      • isReflexive : Bool

                                                        An inductive type is called reflexive if it has at least one constructor that takes as an argument a function returning the same type we are defining. Consider the type:

                                                        inductive WideTree where
                                                        | branch: (Nat -> WideTree) -> WideTree
                                                        | leaf: WideTree
                                                        

                                                        this is reflexive due to the presence of the branch : (Nat -> WideTree) -> WideTree constructor.

                                                        See also: 'Inductive Definitions in the system Coq Rules and Properties' by Christine Paulin-Mohring Section 2.2, Definition 3

                                                      • isNested : Bool

                                                        An inductive definition T is nested when there is a constructor with an argument x : F T, where F : Type → Type is some suitably behaved (ie strictly positive) function (Eg Array T, List T, T × T, ...).

                                                      Instances For
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        @[export lean_mk_inductive_val]
                                                        def Lean.mkInductiveValEx (name : Lake.Name) (levelParams : List Lake.Name) (type : Lean.Expr) (numParams : Nat) (numIndices : Nat) (all : List Lake.Name) (ctors : List Lake.Name) (isRec : Bool) (isUnsafe : Bool) (isReflexive : Bool) (isNested : Bool) :
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[export lean_inductive_val_is_rec]
                                                          Equations
                                                          • v.isRecEx = v.isRec
                                                          Instances For
                                                            @[export lean_inductive_val_is_unsafe]
                                                            Equations
                                                            • v.isUnsafeEx = v.isUnsafe
                                                            Instances For
                                                              @[export lean_inductive_val_is_reflexive]
                                                              Equations
                                                              • v.isReflexiveEx = v.isReflexive
                                                              Instances For
                                                                @[export lean_inductive_val_is_nested]
                                                                Equations
                                                                • v.isNestedEx = v.isNested
                                                                Instances For
                                                                  Equations
                                                                  • v.numCtors = v.ctors.length
                                                                  Instances For
                                                                    • name : Lake.Name
                                                                    • levelParams : List Lake.Name
                                                                    • type : Lean.Expr
                                                                    • induct : Lake.Name

                                                                      Inductive type this constructor is a member of

                                                                    • cidx : Nat

                                                                      Constructor index (i.e., Position in the inductive declaration)

                                                                    • numParams : Nat

                                                                      Number of parameters in inductive datatype.

                                                                    • numFields : Nat

                                                                      Number of fields (i.e., arity - nparams)

                                                                    • isUnsafe : Bool
                                                                    Instances For
                                                                      Equations
                                                                      • Lean.instInhabitedConstructorVal = { default := { toConstantVal := default, induct := default, cidx := default, numParams := default, numFields := default, isUnsafe := default } }
                                                                      @[export lean_mk_constructor_val]
                                                                      def Lean.mkConstructorValEx (name : Lake.Name) (levelParams : List Lake.Name) (type : Lean.Expr) (induct : Lake.Name) (cidx : Nat) (numParams : Nat) (numFields : Nat) (isUnsafe : Bool) :
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        @[export lean_constructor_val_is_unsafe]
                                                                        Equations
                                                                        • v.isUnsafeEx = v.isUnsafe
                                                                        Instances For

                                                                          Information for reducing a recursor

                                                                          • ctor : Lake.Name

                                                                            Reduction rule for this Constructor

                                                                          • nfields : Nat

                                                                            Number of fields (i.e., without counting inductive datatype parameters)

                                                                          • rhs : Lean.Expr

                                                                            Right hand side of the reduction rule

                                                                          Instances For
                                                                            Equations
                                                                            • name : Lake.Name
                                                                            • levelParams : List Lake.Name
                                                                            • type : Lean.Expr
                                                                            • List of all inductive datatypes in the mutual declaration that generated this recursor

                                                                            • numParams : Nat

                                                                              Number of parameters

                                                                            • numIndices : Nat

                                                                              Number of indices

                                                                            • numMotives : Nat

                                                                              Number of motives

                                                                            • numMinors : Nat

                                                                              Number of minor premises

                                                                            • A reduction for each Constructor

                                                                            • k : Bool

                                                                              It supports K-like reduction. A recursor is said to support K-like reduction if one can assume it behaves like Eq under axiom K --- that is, it has one constructor, the constructor has 0 arguments, and it is an inductive predicate (ie, it lives in Prop).

                                                                              Examples of inductives with K-like reduction is Eq, Acc, and And.intro. Non-examples are exists (where the constructor has arguments) and Or.intro (which has multiple constructors).

                                                                            • isUnsafe : Bool
                                                                            Instances For
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              @[export lean_mk_recursor_val]
                                                                              def Lean.mkRecursorValEx (name : Lake.Name) (levelParams : List Lake.Name) (type : Lean.Expr) (all : List Lake.Name) (numParams : Nat) (numIndices : Nat) (numMotives : Nat) (numMinors : Nat) (rules : List Lean.RecursorRule) (k : Bool) (isUnsafe : Bool) :
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                @[export lean_recursor_k]
                                                                                Equations
                                                                                • v.kEx = v.k
                                                                                Instances For
                                                                                  @[export lean_recursor_is_unsafe]
                                                                                  Equations
                                                                                  • v.isUnsafeEx = v.isUnsafe
                                                                                  Instances For
                                                                                    Equations
                                                                                    • v.getMajorIdx = v.numParams + v.numMotives + v.numMinors + v.numIndices
                                                                                    Instances For
                                                                                      Equations
                                                                                      • v.getFirstIndexIdx = v.numParams + v.numMotives + v.numMinors
                                                                                      Instances For
                                                                                        Equations
                                                                                        • v.getFirstMinorIdx = v.numParams + v.numMotives
                                                                                        Instances For
                                                                                          Equations
                                                                                          • v.getInduct = v.name.getPrefix
                                                                                          Instances For
                                                                                            Instances For
                                                                                              Equations
                                                                                              @[export lean_mk_quot_val]
                                                                                              def Lean.mkQuotValEx (name : Lake.Name) (levelParams : List Lake.Name) (type : Lean.Expr) (kind : Lean.QuotKind) :
                                                                                              Equations
                                                                                              • Lean.mkQuotValEx name levelParams type kind = { name := name, levelParams := levelParams, type := type, kind := kind }
                                                                                              Instances For
                                                                                                @[export lean_quot_val_kind]
                                                                                                Equations
                                                                                                • v.kindEx = v.kind
                                                                                                Instances For

                                                                                                  Information associated with constant declarations.

                                                                                                  Instances For
                                                                                                    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
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          Equations
                                                                                                          • d.name = d.toConstantVal.name
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                            • d.levelParams = d.toConstantVal.levelParams
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                              • d.numLevelParams = d.levelParams.length
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                • d.type = d.toConstantVal.type
                                                                                                                Instances For
                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  Instances For
                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      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
                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For

                                                                                                                                List of all (including this one) declarations in the same mutual block.

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