Skip to content
Snippets Groups Projects
Commit 13da2867 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Set `Hint Mode` for `FinSet`.

parent ebb89887
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 0 deletions
theories/base.v
+ 2
− 0
View file @ 13da2867
...@@ -1468,6 +1468,8 @@ Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C, ...@@ -1468,6 +1468,8 @@ Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X; elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X;
NoDup_elements (X : C) : NoDup (elements X) NoDup_elements (X : C) : NoDup (elements X)
}. }.
Global Hint Mode FinSet - ! - - - - - - - - : typeclass_instances.
Class Size C := size: C → nat. Class Size C := size: C → nat.
Global Hint Mode Size ! : typeclass_instances. Global Hint Mode Size ! : typeclass_instances.
Global Arguments size {_ _} !_ / : simpl nomatch, assert. Global Arguments size {_ _} !_ / : simpl nomatch, assert.
......
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