tactic.monotonicity.basic

source

structure tactic.interactive.mono_cfg :

Type

unify : bool

Instances for tactic.interactive.mono_cfg

tactic.interactive.mono_cfg.has_sizeof_inst
tactic.interactive.mono_cfg.inhabited

source

@[protected, instance]

def tactic.interactive.mono_cfg.inhabited :

inhabited tactic.interactive.mono_cfg

source

@[protected, instance]

def tactic.interactive.mono_selection.decidable_eq :

decidable_eq tactic.interactive.mono_selection

source

inductive tactic.interactive.mono_selection :

Type

left : tactic.interactive.mono_selection
right : tactic.interactive.mono_selection
both : tactic.interactive.mono_selection

Instances for tactic.interactive.mono_selection

tactic.interactive.mono_selection.has_sizeof_inst
tactic.interactive.mono_selection.has_reflect
tactic.interactive.mono_selection.inhabited
tactic.interactive.mono_selection.has_to_format

source

@[protected, instance]

def tactic.interactive.mono_selection.inhabited :

inhabited tactic.interactive.mono_selection

source

@[protected, instance]

meta def tactic.interactive.mono_selection.has_reflect :

has_reflect tactic.interactive.mono_selection

source

meta def tactic.interactive.compare (opt : tactic.interactive.mono_cfg) (e₀ e₁ : expr) :

tactic unit

source

meta def tactic.interactive.find_one_difference (opt : tactic.interactive.mono_cfg) :

list expr → list expr → tactic (list expr × expr × expr × list expr)

source

def tactic.interactive.last_two {α : Type u_1} (l : list α) :

option (α × α)

Equations

tactic.interactive.last_two l = tactic.interactive.last_two._match_1 l.reverse
tactic.interactive.last_two._match_1 (x₁ :: x₀ :: _x) = option.some (x₀, x₁)
tactic.interactive.last_two._match_1 [hd] = option.none
tactic.interactive.last_two._match_1 list.nil = option.none

source

meta def tactic.interactive.match_imp :

expr → tactic (expr × expr)

source

meta def tactic.interactive.same_operator :

expr → expr → bool

source

meta def tactic.interactive.get_operator (e : expr) :

option name

source

meta def tactic.interactive.monotonicity.check_rel (l r : expr) :

tactic (option name)

source

@[reducible]

def tactic.interactive.mono_key :

Type

Equations

tactic.interactive.mono_key = (with_bot name × with_bot name)

source

@[protected, instance]

meta def tactic.interactive.mono_key.has_lt :

has_lt tactic.interactive.mono_key

source

meta def tactic.interactive.mono_head_candidates :

ℕ → list expr → expr → tactic tactic.interactive.mono_key

source

meta def tactic.interactive.monotonicity.check (lm_n : name) :

tactic tactic.interactive.mono_key

source

@[protected, instance]

meta def tactic.interactive.mono_selection.has_to_format :

has_to_format tactic.interactive.mono_selection

source

meta def tactic.interactive.side :

lean.parser tactic.interactive.mono_selection

source

meta def tactic.interactive.monotonicity.attr :

user_attribute (native.rb_lmap tactic.interactive.mono_key name) (option tactic.interactive.mono_key × tactic.interactive.mono_selection)

source

meta def tactic.interactive.filter_instances (e : tactic.interactive.mono_selection) (ns : list name) :

tactic (list name)

source

meta def tactic.interactive.get_monotonicity_lemmas (k : expr) (e : tactic.interactive.mono_selection) :

tactic (list name)