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.

        @[inline]

        Valid identifier names

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[inline]
            Equations
            Instances For
              Equations
              Instances For
                @[inline]
                Equations
                Instances For
                  @[inline]
                  Equations
                  Instances For
                    Equations
                    Instances For
                      Equations
                      Instances For
                        @[inline]
                        Equations
                        Instances For
                          @[inline]
                          Equations
                          Instances For
                            Equations
                            Instances For
                              @[export lean_is_inaccessible_user_name]
                              Equations
                              • (pre.str s).isInaccessibleUserName = (s.contains '✝' || s == "_inaccessible")
                              • (p.num i).isInaccessibleUserName = p.isInaccessibleUserName
                              • x.isInaccessibleUserName = false
                              Instances For

                                Creates a round-trippable string name component if possible, otherwise returns none. Names that are valid identifiers are not escaped, and otherwise, if they do not contain », they are escaped.

                                • If force is true, then even valid identifiers are escaped.
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def Lean.Name.toStringWithSep (sep : String) (escape : Bool) (n : Lake.Name) (isToken : optParam (StringBool) fun (x : String) => false) :

                                  Uses the separator sep (usually ".") to combine the components of the Name into a string. See the documentation for Name.toString for an explanation of escape and isToken.

                                  Equations
                                  Instances For
                                    Equations
                                    Instances For
                                      def Lean.Name.toString (n : Lake.Name) (escape : optParam Bool true) (isToken : optParam (StringBool) fun (x : String) => false) :

                                      Converts a name to a string.

                                      • If escape is true, then escapes name components using « and » to ensure that those names that can appear in source files round trip. Names with number components, anonymous names, and names containing » might not round trip. Furthermore, "pseudo-syntax" produced by the delaborator, such as _, #0 or ?u, is not escaped.
                                      • The optional isToken function is used when escape is true to determine whether more escaping is necessary to avoid parser tokens. The insertion algorithm works so long as parser tokens do not themselves contain « or ».
                                      Equations
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations
                                          Equations
                                          Instances For
                                            Equations
                                            • (pre.str s).capitalize = pre.str s.capitalize
                                            • x.capitalize = x
                                            Instances For
                                              Equations
                                              Instances For

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

                                                Equations
                                                • x.eraseSuffix? Lean.Name.anonymous = some x
                                                • (p.str s).eraseSuffix? (p'.str s') = if (s == s') = true then p.eraseSuffix? p' else none
                                                • (p.num s).eraseSuffix? (p'.num s') = if (s == s') = true then p.eraseSuffix? p' else none
                                                • x✝.eraseSuffix? x = none
                                                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
                                                    • n.appendAfter suffix = n.modifyBase fun (x : Lake.Name) => match x with | p.str s => p.mkStr (s ++ suffix) | n => n.mkStr suffix
                                                    Instances For
                                                      @[export lean_name_append_index_after]
                                                      Equations
                                                      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
                                                          • g.curr = g.namePrefix.mkNum g.idx
                                                          Instances For
                                                            @[inline]
                                                            Equations
                                                            • g.next = { namePrefix := g.namePrefix, idx := g.idx + 1 }
                                                            Instances For
                                                              @[inline]
                                                              Equations
                                                              • g.mkChild = ({ namePrefix := g.namePrefix.mkNum g.idx, idx := 1 }, { namePrefix := g.namePrefix, idx := g.idx + 1 })
                                                              Instances For
                                                                Instances
                                                                  Equations
                                                                  Instances For
                                                                    Equations
                                                                    Equations
                                                                    • Lean.Syntax.instReprTSyntax = { reprPrec := Lean.Syntax.reprTSyntax✝ }
                                                                    @[reducible, inline]
                                                                    Equations
                                                                    Instances For
                                                                      @[reducible, inline]
                                                                      Equations
                                                                      Instances For
                                                                        @[reducible, inline]
                                                                        Equations
                                                                        Instances For
                                                                          @[reducible, inline]
                                                                          Equations
                                                                          Instances For
                                                                            @[reducible, inline]
                                                                            Equations
                                                                            Instances For
                                                                              @[reducible, inline]
                                                                              Equations
                                                                              Instances For
                                                                                @[reducible, inline]
                                                                                Equations
                                                                                Instances For
                                                                                  @[reducible, inline]
                                                                                  Equations
                                                                                  Instances For
                                                                                    @[reducible, inline]
                                                                                    Equations
                                                                                    Instances For
                                                                                      @[reducible, inline]
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[reducible, inline]
                                                                                        Equations
                                                                                        Instances For
                                                                                          @[reducible, inline]
                                                                                          Equations
                                                                                          Instances For
                                                                                            Equations
                                                                                            • Lean.TSyntax.instCoeConsSyntaxNodeKindNil = { coe := fun (stx : Lean.TSyntax k) => { raw := stx.raw } }
                                                                                            Equations
                                                                                            • Lean.TSyntax.instCoeConsSyntaxNodeKind = { coe := fun (stx : Lean.TSyntax ks) => { raw := stx.raw } }
                                                                                            Equations
                                                                                            Equations
                                                                                            • Lean.TSyntax.instCoeDepTermMkIdentIdent = { coe := { raw := Lean.Syntax.ident info ss n res } }
                                                                                            Equations
                                                                                            • Lean.TSyntax.Compat.instCoeTailSyntax = { 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 (x1 x2 : Lean.TSyntax k) => x1.raw == x2.raw }
                                                                                                Equations
                                                                                                Instances For
                                                                                                  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

                                                                                                        Replaces the trailing whitespace in stx, if any, with an empty substring.

                                                                                                        The trailing substring's startPos and str are preserved in order to ensure that the result could have been produced by the parser, in case any syntax consumers rely on such an assumption.

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

                                                                                                            Return the first atom/identifier that has position information

                                                                                                            Equations
                                                                                                            • target.copyHeadTailInfoFrom source = (target.setHeadInfo source.getHeadInfo).setTailInfo source.getTailInfo
                                                                                                            Instances For

                                                                                                              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
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      Equations
                                                                                                                                      • Lean.Syntax.instCoeArraySepArray = { coe := Lean.Syntax.SepArray.ofElems }

                                                                                                                                      Constructs a typed separated array from elements. The given array does not include the separators.

                                                                                                                                      Like Syntax.SepArray.ofElems but for typed syntax.

                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        Equations
                                                                                                                                        • Lean.Syntax.instCoeTSyntaxArrayTSepArray = { coe := Lean.Syntax.TSepArray.ofElems }

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

                                                                                                                                        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.
                                                                                                                                              • Lean.Syntax.isLit? litKind stx = none
                                                                                                                                              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
                                                                                                                                                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
                                                                                                                                                        • stx.toNat = match stx.isNatLit? with | some val => val | none => 0
                                                                                                                                                        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 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
                                                                                                                                                              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
                                                                                                                                                                    Equations
                                                                                                                                                                    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

                                                                                                                                                                          Converts a String to a hierarchical Name after splitting it at the dots.

                                                                                                                                                                          "a.b".toName is the name a.b, not «a.b». For the latter, use Name.mkSimple.

                                                                                                                                                                          Equations
                                                                                                                                                                          • s.toName = s.toSubstring.toName
                                                                                                                                                                          Instances For
                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        Equations
                                                                                                                                                                                        • stx.getOptionalIdent? = match stx.getOptional? with | some stx => some stx.getId | none => none
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                Equations
                                                                                                                                                                                                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
                                                                                                                                                                                                            class Lean.Quote (α : Type) (k : optParam Lean.SyntaxNodeKind `term) :

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

                                                                                                                                                                                                            Instances
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              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
                                                                                                                                                                                                                      @[reducible, inline]
                                                                                                                                                                                                                      abbrev Array.getSepElems {α : Type u_1} (as : Array α) :
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          • a.filterSepElems p = (a.filterSepElemsM p).run
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              • a.mapSepElems f = (a.mapSepElemsM f).run
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                • sa.getElems = sa.elemsAndSeps.getSepElems
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    • sa.push e = if sa.elemsAndSeps.isEmpty = true then { elemsAndSeps := #[e.raw] } else { elemsAndSeps := (sa.elemsAndSeps.push (Lean.mkAtom sep)).push e.raw }
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      • Lean.Syntax.instEmptyCollectionSepArray = { emptyCollection := { elemsAndSeps := } }
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      • Lean.Syntax.instEmptyCollectionTSepArray = { emptyCollection := { elemsAndSeps := } }
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      • Lean.Syntax.instCoeOutSepArrayArray = { coe := Lean.Syntax.SepArray.getElems }
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      • Lean.Syntax.instCoeOutTSepArrayTSyntaxArray = { coe := Lean.Syntax.TSepArray.getElems }
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      • Lean.Syntax.instCoeOutTSyntaxArrayArray = { coe := fun (a : Lean.TSyntaxArray k) => a.raw }
                                                                                                                                                                                                                                      Equations

                                                                                                                                                                                                                                      Helper functions for manipulating interpolated strings #

                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        • stx.getSepArgs = stx.getArgs.getSepElems
                                                                                                                                                                                                                                        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
                                                                                                                                                                                                                                              def Lean.TSyntax.getDocString (stx : Lean.TSyntax `Lean.Parser.Command.docComment) :
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              • stx.getDocString = match stx.raw[1] with | Lean.Syntax.atom info val => val.extract 0 (val.endPos - { byteIdx := 2 }) | x => ""
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                  Controls which new mvars are turned in to goals by the apply tactic.

                                                                                                                                                                                                                                                  • nonDependentFirst mvars that don't depend on other goals appear first in the goal list.
                                                                                                                                                                                                                                                  • nonDependentOnly only mvars that don't depend on other goals are added to goal list.
                                                                                                                                                                                                                                                  • all all unassigned mvars are added to the goal list.
                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                    Configures the behaviour of the apply tactic.

                                                                                                                                                                                                                                                    • synthAssignedInstances : Bool

                                                                                                                                                                                                                                                      If synthAssignedInstances is true, then apply will synthesize instance implicit arguments even if they have assigned by isDefEq, and then check whether the synthesized value matches the one inferred. The congr tactic sets this flag to false.

                                                                                                                                                                                                                                                    • allowSynthFailures : Bool

                                                                                                                                                                                                                                                      If allowSynthFailures is true, then apply will return instance implicit arguments for which typeclass search failed as new goals.

                                                                                                                                                                                                                                                    • approx : Bool

                                                                                                                                                                                                                                                      If approx := true, then we turn on isDefEq approximations. That is, we use the approxDefEq combinator.

                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                      Configures the behaviour of the omega tactic.

                                                                                                                                                                                                                                                      • splitDisjunctions : Bool

                                                                                                                                                                                                                                                        Split disjunctions in the context.

                                                                                                                                                                                                                                                        Note that with splitDisjunctions := false omega will not be able to solve x = y goals as these are usually handled by introducing ¬ x = y as a hypothesis, then replacing this with x < y ∨ x > y.

                                                                                                                                                                                                                                                        On the other hand, omega does not currently detect disjunctions which, when split, introduce no new useful information, so the presence of irrelevant disjunctions in the context can significantly increase run time.

                                                                                                                                                                                                                                                      • splitNatSub : Bool

                                                                                                                                                                                                                                                        Whenever ((a - b : Nat) : Int) is found, register the disjunction b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0 for later splitting.

                                                                                                                                                                                                                                                      • splitNatAbs : Bool

                                                                                                                                                                                                                                                        Whenever Int.natAbs a is found, register the disjunction 0 ≤ a ∧ Int.natAbs a = a ∨ a < 0 ∧ Int.natAbs a = - a for later splitting.

                                                                                                                                                                                                                                                      • splitMinMax : Bool

                                                                                                                                                                                                                                                        Whenever min a b or max a b is found, rewrite in terms of the definition if a ≤ b ..., for later case splitting.

                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                        inductive Lean.Meta.CheckTactic.CheckGoalType {α : Sort u} (val : α) :

                                                                                                                                                                                                                                                        Type used to lift an arbitrary value into a type parameter so it can appear in a proof goal.

                                                                                                                                                                                                                                                        It is used by the #check_tactic command.

                                                                                                                                                                                                                                                        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