mathlib documentation

core / init.meta.well_founded_tactics

theorem nat.lt_add_of_zero_lt_left (a b : ) (h : 0 < b) :
a < a + b
theorem nat.zero_lt_one_add (a : ) :
0 < 1 + a
theorem nat.lt_add_right (a b c : ) :
a < ba < b + c
theorem nat.lt_add_left (a b c : ) :
a < ba < c + b
@[protected]
def psum.alt.sizeof {α : Type u} {β : Type v} [has_sizeof α] [has_sizeof β] :
psum α β
Equations
@[protected, reducible]
def psum.has_sizeof_alt (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :
Equations
meta structure well_founded_tactics  :
Type

Argument for using_well_founded

The tactic rel_tac has to synthesize an element of type (has_well_founded A). The two arguments are: a local representing the function being defined by well founded recursion, and a list of recursive equations. The equations can be used to decide which well founded relation should be used.

The tactic dec_tac has to synthesize decreasing proofs.