Commit c60c5192 authored by Robbert Krebbers's avatar Robbert Krebbers

Add a constant `tc_opaque` for type class opaque definitions.

parent fe8930b6
Pipeline #4598 passed with stages
in 10 minutes and 2 seconds
......@@ -24,6 +24,13 @@ Arguments unseal {_ _} _ : assert.
Arguments seal_eq {_ _} _ : assert.
Unset Primitive Projections.
(** Typeclass opaque definitions *)
(* The constant [tc_opaque] is used to make definitions opaque for just type
class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
Definition tc_opaque {A} (x : A) : A := x.
Typeclasses Opaque tc_opaque.
Arguments tc_opaque {_} _ /.
(* Below we define type class versions of the common logical operators. It is
important to note that we duplicate the definitions, and do not declare the
existing logical operators as type classes. That is, we do not say:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment