Stream: Coq users

Topic: ✔ Find term of a given type

Patrick Nicodemus (Sep 29 2022 at 13:24):

Can I use "set" or something similar to match on a term of a given type in the goal? For example, say that my goal contains a subterm t of type bool, can I do something like "set z : bool := _ " or similar to set z := t?

Gaëtan Gilbert (Sep 29 2022 at 13:30):

Goal 1 = 1 /\ true = true.
set (some_bool := _ : bool).
(* some_bool := (true : bool) : bool |- 1 = 1 /\ some_bool = some_bool *)

(* cbv beta will get rid of the extra cast with usually no or little reduction *)
cbv beta in some_bool.

Patrick Nicodemus (Sep 29 2022 at 13:30):

Nice, thank you!

Notification Bot (Sep 29 2022 at 13:31):

Patrick Nicodemus has marked this topic as resolved.

Last updated: Oct 01 2023 at 19:01 UTC