Specification language
match
in
type_scope
function_scope
Arguments
Proofs
Proof using
Scheme
Derive
Inversion
dependent destruction
dependent induction
lra
lia
nra
nia
psatz
zify
nsatz
Type
L
Using Coq
Functional
coqrc
-vos
Appendix
add_bottom
add_top
bypass_check(guard)
bypass_check(positivity)
bypass_check(universes)
canonical
Cumulative
deprecated
export
global
local
Monomorphic
NonCumulative
nonuniform
Polymorphic
Private
private(matching)
program
Program
projections(primitive)
refine
reversible
universes(cumulative)
universes(polymorphic)
universes(template)
using