def Lean.Parser.Tactic.unknown : Lean.Parser.Parser

Equations

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

def Lean.Parser.Tactic.nestedTactic : Lean.Parser.Parser

Equations

• Lean.Parser.Tactic.nestedTactic = Lean.Parser.Tactic.tacticSeqBracketed

def Lean.Parser.Tactic.matchRhs : Lean.Parser.Parser

Equations

• Lean.Parser.Tactic.matchRhs = HOrElse.hOrElse Lean.Parser.Term.hole fun x => HOrElse.hOrElse Lean.Parser.Term.syntheticHole fun x => Lean.Parser.Tactic.tacticSeq

def Lean.Parser.Tactic.matchAlts : Lean.Parser.Parser

Equations

• Lean.Parser.Tactic.matchAlts = Lean.Parser.Term.matchAlts Lean.Parser.Tactic.matchRhs

def Lean.Parser.Tactic.match : Lean.Parser.Parser

match performs case analysis on one or more expressions. See Induction and Recursion. The syntax for the match tactic is the same as term-mode match, except that the match arms are tactics instead of expressions.

example (n : Nat) : n = n := by
  match n with
  | 0 => rfl
  | i+1 => simp

Equations

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

def Lean.Parser.Tactic.introMatch : Lean.Parser.Parser

The tactic

intro
| pat1 => tac1
| pat2 => tac2

is the same as:

intro x
match x with
| pat1 => tac1
| pat2 => tac2

That is, intro can be followed by match arms and it introduces the values while doing a pattern match. This is equivalent to fun with match arms in term mode.

Equations

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

def Lean.Parser.Tactic.decide : Lean.Parser.Parser

decide will attempt to prove a goal of type p by synthesizing an instance of Decidable p and then evaluating it to isTrue ... Because this uses kernel computation to evaluate the term, it may not work in the presence of definitions by well founded recursion, since this requires reducing proofs.

example : 2 + 2 ≠ 5 := by decide

Equations

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

def Lean.Parser.Tactic.nativeDecide : Lean.Parser.Parser

native_decide will attempt to prove a goal of type p by synthesizing an instance of Decidable p and then evaluating it to isTrue ... Unlike decide, this uses #eval to evaluate the decidability instance.

This should be used with care because it adds the entire lean compiler to the trusted part, and the axiom ofReduceBool will show up in #print axioms for theorems using this method or anything that transitively depends on them. Nevertheless, because it is compiled, this can be significantly more efficient than using decide, and for very large computations this is one way to run external programs and trust the result.

example : (List.range 1000).length = 1000 := by native_decide

Equations

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