mathlib documentation

core.init.meta.ref

source
meta constant tactic.ref (α : Type u) :
Type u

A ref performs the role of a mutable variable within a tactic.

source
meta constant tactic.using_new_ref {α : Type u} {β : Type v} (a : α) (t : tactic.ref α → tactic β) :
tactic β

Create a new reference r with initial value a, execute t r, and then delete r.

source
meta constant tactic.read_ref {α : Type u} (a : tactic.ref α) :
tactic α

Read the value stored in the given reference.

source
meta constant tactic.write_ref {α : Type u} (a : tactic.ref α) (a_1 : α) :
tactic unit

Update the value stored in the given reference.