Documentation

Init.Meta

@[extern lean_get_githash]
@[extern lean_version_get_is_release]
@[extern lean_version_get_special_desc]

Additional version description like "nightly-2018-03-11"

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
        @[extern lean_internal_is_stage0]
        @[extern lean_internal_has_llvm_backend]

        This function can be used to detect whether the compiler has support for generating LLVM instead of C. It is used by lake instead of the --features flag in order to avoid having to run a compiler for this every time on startup. See #2572.

        Valid identifier names

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

                            eraseSuffix? n s return n' if n is of the form n == n' ++ s.

                            Equations
                            Instances For
                              @[inline]

                              Remove macros scopes, apply f, and put them back

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[export lean_name_append_after]
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[export lean_name_append_index_after]
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[export lean_name_append_before]
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem Lean.Name.beq_iff_eq {m : Lake.Name} {n : Lake.Name} :
                                      (m == n) = true m = n
                                      Equations
                                      @[inline]
                                      Equations
                                      Instances For
                                        @[inline]
                                        Equations
                                        Instances For
                                          @[inline]
                                          Equations
                                          Instances For
                                            Instances
                                              Equations
                                              Instances For
                                                Equations
                                                Equations
                                                • Lean.Syntax.instReprTSyntax = { reprPrec := Lean.Syntax.reprTSyntax✝ }
                                                @[inline, reducible]
                                                Equations
                                                Instances For
                                                  @[inline, reducible]
                                                  Equations
                                                  Instances For
                                                    @[inline, reducible]
                                                    Equations
                                                    Instances For
                                                      @[inline, reducible]
                                                      Equations
                                                      Instances For
                                                        @[inline, reducible]
                                                        Equations
                                                        Instances For
                                                          @[inline, reducible]
                                                          Equations
                                                          Instances For
                                                            @[inline, reducible]
                                                            Equations
                                                            Instances For
                                                              @[inline, reducible]
                                                              Equations
                                                              Instances For
                                                                @[inline, reducible]
                                                                Equations
                                                                Instances For
                                                                  @[inline, reducible]
                                                                  Equations
                                                                  Instances For
                                                                    @[inline, reducible]
                                                                    Equations
                                                                    Instances For
                                                                      @[inline, reducible]
                                                                      Equations
                                                                      Instances For
                                                                        Equations
                                                                        • Lean.TSyntax.instCoeTSyntaxConsSyntaxNodeKindNil = { coe := fun (stx : Lean.TSyntax k) => { raw := stx.raw } }
                                                                        Equations
                                                                        • Lean.TSyntax.instCoeTSyntaxConsSyntaxNodeKind = { coe := fun (stx : Lean.TSyntax ks) => { raw := stx.raw } }
                                                                        Equations
                                                                        Equations
                                                                        • Lean.TSyntax.instCoeDepTermMkConsSyntaxNodeKindMkStr1NilIdentIdent = { coe := { raw := Lean.Syntax.ident info ss n res } }
                                                                        Equations
                                                                        • Lean.TSyntax.Compat.instCoeTailSyntaxTSyntax = { coe := fun (s : Lean.Syntax) => { raw := s } }
                                                                        Instances For
                                                                          Equations
                                                                          • Lean.TSyntax.Compat.instCoeTailArraySyntaxTSyntaxArray = { coe := Lean.TSyntaxArray.mk }
                                                                          Instances For

                                                                            Compare syntax structures modulo source info.

                                                                            Equations
                                                                            • Lean.Syntax.instBEqTSyntax = { beq := fun (x x_1 : Lean.TSyntax k) => x.raw == x_1.raw }
                                                                            Equations
                                                                            Instances For

                                                                              Return substring of original input covering stx. Result is meaningful only if all involved SourceInfo.originals refer to the same string (as is the case after parsing).

                                                                              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
                                                                                    Instances For
                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For

                                                                                        Return the first atom/identifier that has position information

                                                                                        Ensure head position is synthetic. The server regards syntax as "original" only if both head and tail info are original.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[inline]
                                                                                          def Lean.withHeadRefOnly {m : TypeType} [Monad m] [Lean.MonadRef m] {α : Type} (x : m α) :
                                                                                          m α

                                                                                          Use the head atom/identifier of the current ref as the ref

                                                                                          Equations
                                                                                          Instances For
                                                                                            partial def Lean.expandMacros (stx : Lean.Syntax) (p : optParam (Lean.SyntaxNodeKindBool) fun (k : Lean.SyntaxNodeKind) => k != `Lean.Parser.Term.byTactic) :

                                                                                            Expand macros in the given syntax. A node with kind k is visited only if p k is true.

                                                                                            Note that the default value for p returns false for by ... nodes. This is a "hack". The tactic framework abuses the macro system to implement extensible tactics. For example, one can define

                                                                                            syntax "my_trivial" : tactic -- extensible tactic
                                                                                            
                                                                                            macro_rules | `(tactic| my_trivial) => `(tactic| decide)
                                                                                            macro_rules | `(tactic| my_trivial) => `(tactic| assumption)
                                                                                            

                                                                                            When the tactic evaluator finds the tactic my_trivial, it tries to evaluate the macro_rule expansions until one "works", i.e., the macro expansion is evaluated without producing an exception. We say this solution is a bit hackish because the term elaborator may invoke expandMacros with (p := fun _ => true), and expand the tactic macros as just macros. In the example above, my_trivial would be replaced with assumption, decide would not be tried if assumption fails at tactic evaluation time.

                                                                                            We are considering two possible solutions for this issue: 1- A proper extensible tactic feature that does not rely on the macro system.

                                                                                            2- Typed macros that know the syntax categories they're working in. Then, we would be able to select which syntactic categories are expanded by expandMacros.

                                                                                            Helper functions for processing Syntax programmatically #

                                                                                            Create an identifier copying the position from src. To refer to a specific constant, use mkCIdentFrom instead.

                                                                                            Equations
                                                                                            Instances For
                                                                                              def Lean.mkIdentFromRef {m : TypeType} [Monad m] [Lean.MonadRef m] (val : Lake.Name) (canonical : optParam Bool false) :
                                                                                              Equations
                                                                                              Instances For

                                                                                                Create an identifier referring to a constant c copying the position from src. This variant of mkIdentFrom makes sure that the identifier cannot accidentally be captured.

                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[export lean_mk_syntax_ident]
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[inline]
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For
                                                                                                                  Equations
                                                                                                                  • Lean.Syntax.instCoeArraySyntaxSepArray = { coe := Lean.Syntax.SepArray.ofElems }
                                                                                                                  Equations

                                                                                                                  Create syntax representing a Lean term application, but avoid degenerate empty applications.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      Equations
                                                                                                                      Instances For

                                                                                                                        Recall that we don't have special Syntax constructors for storing numeric and string atoms. The idea is to have an extensible approach where embedded DSLs may have new kind of atoms and/or different ways of representing them. So, our atoms contain just the parsed string. The main Lean parser uses the kind numLitKind for storing natural numbers that can be encoded in binary, octal, decimal and hexadecimal format. isNatLit implements a "decoder" for Syntax objects representing these numerals.

                                                                                                                        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

                                                                                                                            Decodes a 'scientific number' string which is consumed by the OfScientific class. Takes as input a string such as 123, 123.456e7 and returns a triple (n, sign, e) with value given by n * 10^-e if sign else n * 10^e.

                                                                                                                            Equations
                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                            Instances For
                                                                                                                              partial def Lean.Syntax.decodeScientificLitVal?.decodeAfterExp (s : String) (i : String.Pos) (val : Nat) (e : Nat) (sign : Bool) (exp : Nat) :
                                                                                                                              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

                                                                                                                                      Decodes a valid string gap after the \. Note that this function matches "\" whitespace+ rather than the more restrictive "\" newline whitespace* since this simplifies the implementation. Justification: this does not overlap with any other sequences beginning with \.

                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        partial def Lean.Syntax.decodeRawStrLitAux (s : String) (i : String.Pos) (num : Nat) :

                                                                                                                                        Takes a raw string literal, counts the number of #'s after the r, and interprets it as a string. The position i should start at 1, which is the character after the leading r. The algorithm is simple: we are given r##...#"...string..."##...# with zero or more #s. By counting the number of leading #'s, we can extract the ...string....

                                                                                                                                        Takes the string literal lexical syntax parsed by the parser and interprets it as a string. This is where escape sequences are processed for example. The string s is is either a plain string literal or a raw string literal.

                                                                                                                                        If it returns none then the string literal is ill-formed, which indicates a bug in the parser. The function is not required to return none if the string literal is ill-formed.

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

                                                                                                                                          If the provided Syntax is a string literal, returns the string it represents.

                                                                                                                                          Even if the Syntax is a str node, the function may return none if its internally ill-formed. The parser should always create well-formed str nodes.

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

                                                                                                                                              Split a name literal (without the backtick) into its dot-separated components. For example, foo.bla.«bo.o»["foo", "bla", "«bo.o»"]. If the literal cannot be parsed, return [].

                                                                                                                                              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
                                                                                                                                                        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
                                                                                                                                                                class Lean.Quote (α : Type) (k : optParam Lean.SyntaxNodeKind `term) :

                                                                                                                                                                Reflect a runtime datum back to surface syntax (best-effort).

                                                                                                                                                                Instances
                                                                                                                                                                  Equations
                                                                                                                                                                  Equations
                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    Equations
                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                    instance Lean.instQuoteProdMkStr1 {α : Type} {β : Type} [Lean.Quote α] [Lean.Quote β] :
                                                                                                                                                                    Lean.Quote (α × β)
                                                                                                                                                                    Equations
                                                                                                                                                                    Equations
                                                                                                                                                                    Equations
                                                                                                                                                                    Equations
                                                                                                                                                                    • One or more equations did not get rendered due to their size.

                                                                                                                                                                    Evaluator for prec DSL

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

                                                                                                                                                                      Evaluator for prio DSL

                                                                                                                                                                      Equations
                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                      Instances For
                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[inline, reducible]
                                                                                                                                                                          abbrev Array.getSepElems {α : Type u_1} (as : Array α) :
                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              Equations
                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                              Instances For
                                                                                                                                                                                Equations
                                                                                                                                                                                • Lean.Syntax.instEmptyCollectionSepArray = { emptyCollection := { elemsAndSeps := } }
                                                                                                                                                                                Equations
                                                                                                                                                                                • Lean.Syntax.instEmptyCollectionTSepArray = { emptyCollection := { elemsAndSeps := } }
                                                                                                                                                                                Equations
                                                                                                                                                                                • Lean.Syntax.instCoeOutSepArrayArraySyntax = { coe := Lean.Syntax.SepArray.getElems }
                                                                                                                                                                                Equations
                                                                                                                                                                                • Lean.Syntax.instCoeOutTSepArrayTSyntaxArray = { coe := Lean.Syntax.TSepArray.getElems }
                                                                                                                                                                                Equations
                                                                                                                                                                                Equations
                                                                                                                                                                                Equations
                                                                                                                                                                                @[inline, reducible]
                                                                                                                                                                                abbrev autoParam (α : Sort u) (tactic : Lean.Syntax) :

                                                                                                                                                                                Gadget for automatic parameter support. This is similar to the optParam gadget, but it uses the given tactic. Like optParam, this gadget only affects elaboration. For example, the tactic will not be invoked during type class resolution.

                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For

                                                                                                                                                                                  Helper functions for manipulating interpolated strings #

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

                                                                                                                                                                                            erw [rules] is a shorthand for rw (config := { transparency := .default }) [rules]. This does rewriting up to unfolding of regular definitions (by comparison to regular rw which only unfolds @[reducible] definitions).

                                                                                                                                                                                            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
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                    simp! is shorthand for simp with autoUnfold := true. This will rewrite with all equation lemmas, which can be used to partially evaluate many definitions.

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

                                                                                                                                                                                                      simp_arith is shorthand for simp with arith := true and decide := true. This enables the use of normalization by linear arithmetic.

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

                                                                                                                                                                                                        simp_arith! is shorthand for simp_arith with autoUnfold := true. This will rewrite with all equation lemmas, which can be used to partially evaluate many definitions.

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

                                                                                                                                                                                                          simp_all! is shorthand for simp_all with autoUnfold := true. This will rewrite with all equation lemmas, which can be used to partially evaluate many definitions.

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

                                                                                                                                                                                                            simp_all_arith combines the effects of simp_all and simp_arith.

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

                                                                                                                                                                                                              simp_all_arith! combines the effects of simp_all, simp_arith and simp!.

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

                                                                                                                                                                                                                dsimp! is shorthand for dsimp with autoUnfold := true. This will rewrite with all equation lemmas, which can be used to partially evaluate many definitions.

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