3
$\begingroup$

Are there any ways to unfold an expression in Coq by a single layer?

I have only come up with this obvious solution:

Parameter  X : Set.
Definition Y := X.
Definition Z := Y.

Goal Z.
  match goal with
  | |- ?h => unfold h
  end.
  (* 
   ================
   Y
   *)
Abort.    

But for sure there are better and more elegant ways to do it.

$\endgroup$
2

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.