Search Rocq packages
max) { row = max } }" @keyup.up="if (row !== null) { row -=1; if (row < 0) { row = null } }" @keyup.right="if (col < 1) col++" @keyup.left="if (col >= 1) col--" :aria-activedescendant="row !== null ? 'package-autocomplete-'+row+'-'+col : null" hx-get="/packages/autocomplete" hx-params="q" hx-trigger="keyup changed, search" hx-target="#header-search-results" hx-indicator="#header-search-indicator" autocomplete="off" >
Standard Library
Learn
Platform
Packages
Community
Consortium
News
Play
Get Started
Search Rocq packages
Learn
Platform
Packages
Community
Consortium
News
Play
Standard Library
Get started
Inductively Defined Types
Thierry Coquand and Christine Paulin-Mohring, International Conference on Computer Logic: 50-66 — 1988
Links
DOI
Springer
Abstract
Inductive types