The extract_lets at
tactic #
This module defines a tactic extract_lets ... at h
that can be used to (in essence) do cases
on a let
expression.
Given a local hypothesis whose type is a let
expression, then lift the let
bindings to be
a new local definition.
Instances For
Check that t
is a let
and then do what's necessary to lift it over the binding
described by mk
.
Instances For
A more limited version of Lean.MVarId.introN
that ensures the goal is a
nested let
expression.
Instances For
The extract_lets at h
tactic takes a local hypothesis of the form h : let x := v; b
and introduces a new local definition x := v
while changing h
to be h : b
. It can be thought
of as being a cases
tactic for let
expressions. It can also be thought of as being like
intros at h
for let
expressions.
For example, if h : let x := 1; x = x
, then extract_lets x at h
introduces x : Nat := 1
and
changes h
to h : x = x
.
Just like intros
, the extract_lets
tactic either takes a list of names, in which case
that specifies the number of let
bindings that must be extracted, or it takes no names, in which
case all the let
bindings are extracted.
The tactic extract_let at ⊢
is a weaker form of intros
that only introduces obvious let
s.