Skip to content

`tc_to_bool` to turn a type class into a Boolean that expresses if there is an instance

Robbert Krebbers requested to merge robbert/bool_of_tc into master

This MR introduces the following function:

(** Given a proposition [P] that is a type class, [bool_of_tc P] will return
[true] iff there is an instance of [P]. *)
Definition bool_of_tc (P : Prop)
  {p : bool} `{TCIf P (TCEq p true) (TCEq p false)} : bool := p.

It's particularly useful in Ltac, where it's sometimes needed to figure out if an instance exists or not. An example use can be found in

Edited by Robbert Krebbers

Merge request reports