I have this function:
Definition bexp x y := bexp_r x y [true].
And I have this goal:
value (bexp  y) = 0 ^ value y
I want to replace the call to
bexp with the underlying
I tried to use the
simpl tactic but it did not replace it.
Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.Sign up to join this community
The tactic you are looking for is probably
unfold. If you write
unfold bexp it will replace it with its body.
In certain cases, unfolding the definition will unfold too much and if you want more control over it you can prove unfolding lemmas instead and rewrite with them.