Library Coq.Classes.Init
Initialization code for typeclasses, setting up the default tactic
for instance search.Require Import Coq.Program.Basics.
Global Typeclasses Opaque id const flip compose arrow impl iff not all.
Apply using the same opacity information as typeclass proof search.
Ltac class_apply c := autoapply c with typeclass_instances.
The unconvertible typeclass, to test that two objects of the same type are
actually different.
#[universes(polymorphic)]
Class Unconvertible (A : Type) (a b : A) := unconvertible : unit.
Ltac unconvertible :=
match goal with
| |- @Unconvertible _ ?x ?y => unify x y with typeclass_instances ; fail 1 "Convertible"
| |- _ => exact tt
end.
#[global]
Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
Class Unconvertible (A : Type) (a b : A) := unconvertible : unit.
Ltac unconvertible :=
match goal with
| |- @Unconvertible _ ?x ?y => unify x y with typeclass_instances ; fail 1 "Convertible"
| |- _ => exact tt
end.
#[global]
Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.