Mathlib.Tactic.Conv

conv in pat => cs runs the conv tactic sequence cs on the first subexpression matching the pattern pat in the target. The converted expression becomes the new target subgoal, like conv => cs.

The arguments in are the same as those as the in pattern. In fact, conv in pat => cs is a macro for conv => pattern pat; cs.

The syntax also supports the occs clause. Example:

conv in (occs := *) x + y => rw [add_comm]

Equations

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

Instances For

source

def Mathlib.Tactic.Conv.dischargeConv :

Lean.ParserDescr

discharge => tac is a conv tactic which rewrites target p to True if tac is a tactic which proves the goal ⊢ p.
discharge without argument returns ⊢ p as a subgoal.

Equations

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

Instances For

source

def Mathlib.Tactic.Conv.elabDischargeConv :

Lean.Elab.Tactic.Tactic

Elaborator for the discharge tactic.

Equations

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

Instances For

source

def Mathlib.Tactic.Conv.convRefine_ :

Lean.ParserDescr

Use refine in conv mode.

Equations

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

Instances For

source

def Mathlib.Tactic.Conv.«command#conv_=>_» :

Lean.ParserDescr

The command #conv tac => e will run a conv tactic tac on e, and display the resulting expression (discarding the proof). For example, #conv rw [true_and] => True ∧ False displays False. There are also shorthand commands for several common conv tactics:

#whnf e is short for #conv whnf => e
#simp e is short for #conv simp => e
#norm_num e is short for #conv norm_num => e
#push_neg e is short for #conv push_neg => e

Equations

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

Instances For

source

def Mathlib.Tactic.Conv.withReducible :

Lean.ParserDescr

with_reducible tacs executes tacs using the reducible transparency setting. In this setting only definitions tagged as [reducible] are unfolded.

Equations

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

Instances For

source

def Mathlib.Tactic.Conv.«command#whnf_» :

Lean.ParserDescr

The command #whnf e evaluates e to Weak Head Normal Form, which means that the "head" of the expression is reduced to a primitive - a lambda or forall, or an axiom or inductive type. It is similar to #reduce e, but it does not reduce the expression completely, only until the first constructor is exposed. For example:

open Nat List
set_option pp.notation false
#whnf [1, 2, 3].map succ
-- cons (succ 1) (map succ (cons 2 (cons 3 nil)))
#reduce [1, 2, 3].map succ
-- cons 2 (cons 3 (cons 4 nil))

The head of this expression is the List.cons constructor, so we can see from this much that the list is not empty, but the subterms Nat.succ 1 and List.map Nat.succ (List.cons 2 (List.cons 3 List.nil)) are still unevaluated. #reduce is equivalent to using #whnf on every subexpression.

Equations

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

Instances For

source

def Mathlib.Tactic.Conv.«command#whnfR_» :

Lean.ParserDescr

The command #whnfR e evaluates e to Weak Head Normal Form with Reducible transparency, that is, it uses whnf but only unfolding reducible definitions.

Equations

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

Instances For

source

def Mathlib.Tactic.Conv.«command#simpOnly_=>__» :

Lean.ParserDescr

#simp => e runs simp on the expression e and displays the resulting expression after simplification.
#simp only [lems] => e runs simp only [lems] on e.
The => is optional, so #simp e and #simp only [lems] e have the same behavior. It is mostly useful for disambiguating the expression e from the lemmas.

Equations

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

Instances For