package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

CS cpattern: (f _), (X in t), (t in X in t), (t as X in t)

OS cpattern: f _, (X in t), (t in X in t), (t as X in t)

OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t