Documentation

Lean.Structure

Instances For
    Equations
    Equations
    • i₁.lt i₂ = i₁.fieldName.quickLt i₂.fieldName
    Instances For
      Instances For
        Equations
        Equations
        • i₁.lt i₂ = i₁.structName.quickLt i₂.structName
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Instances For
              Equations
              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
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Get direct field names for the given structure.

                    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

                        If fieldName represents the relation to a parent structure S, return S

                        Equations
                        Instances For

                          Return immediate parent structures

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

                            Return all parent structures

                            Equations
                            Instances For
                              partial def Lean.findField? (env : Lean.Environment) (structName : Lake.Name) (fieldName : Lake.Name) :

                              findField? env S fname. If fname is defined in a parent S' of S, return S'

                              def Lean.getStructureFieldsFlattened (env : Lean.Environment) (structName : Lake.Name) (includeSubobjectFields : optParam Bool true) :

                              Return field names for the given structure, including "flattened" fields from parent structures. To omit toParent projections, set includeSubobjectFields := false.

                              For example, given Bar such that

                              structure Foo where a : Nat
                              structure Bar extends Foo where b : Nat
                              

                              return #[toFoo,a,b] or #[a,b] with subobject fields omitted.

                              Equations
                              Instances For
                                def Lean.isStructure (env : Lean.Environment) (constName : Lake.Name) :

                                Return true if constName is the name of an inductive datatype created using the structure or class commands.

                                We perform the check by testing whether auxiliary projection functions have been created.

                                Equations
                                Instances For
                                  Equations
                                  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
                                          partial def Lean.getPathToBaseStructureAux (env : Lean.Environment) (baseStructName : Lake.Name) (structName : Lake.Name) (path : List Lake.Name) :
                                          def Lean.getPathToBaseStructure? (env : Lean.Environment) (baseStructName : Lake.Name) (structName : Lake.Name) :

                                          If baseStructName is an ancestor structure for structName, then return a sequence of projection functions to go from structName to baseStructName.

                                          Equations
                                          Instances For

                                            Return true iff constName is the a non-recursive inductive datatype that has only one constructor.

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

                                              Return number of fields for a structure-like type

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