Tactic Examples

We show many examples of using tactics. The results are of the form m ≤ n where m and n are natural numbers.

The apply tactic and repeat tactic combinator

def someNat : Nat

Equations

• someNat = (Nat.succ 4).succ

def anotherNat : Nat

Equations

• anotherNat = (Nat.add 2 Nat.zero.succ).succ

def tacticNat_le : Lean.ParserDescr

Equations

• tacticNat_le = Lean.ParserDescr.node `tacticNat_le 1024 (Lean.ParserDescr.nonReservedSymbol "nat_le" false)

def tacticRepeating_Finish_with_ : Lean.ParserDescr

Equations

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