CoqTricks - wjzz/NotesAndCheatsheets GitHub Wiki

Strong specifications

Find info about a notation

Locate "{ _ | _ }".

returns

Notation            Scope     
"{ x  |  P }" := sig (fun x => P)
                     : type_scope
                     (default interpretation)

Search libraries

SearchRewrite ((_ ++ _) ++ _).