sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page
- The type of constructions
- Functions for dealing with constr terms.
- Term constructors.
- Concrete type for making pattern-matching.
- Term destructors
- Equality
- Extension of Context with declarations on constr
- Relocation and substitution
- Functionals working on expressions canonically abstracted over a local context (possibly with let-ins)
- Functionals working on the immediate subterm of a construction
- Hashconsing
package rocq-runtime
-
-
Library
btauto_plugin
-
Library
byte_config
-
Library
cc_core_plugin
-
Library
cc_plugin
-
Library
derive_plugin
-
Library
extraction_plugin
-
Library
firstorder_plugin
-
Library
ltac2_ltac1_plugin
-
Library
ltac2_plugin
-
-
Library
ltac_plugin
-
-
Library
nsatz_plugin
-
Library
number_string_notation_plugin
-
Library
ring_plugin
-
Library
rocq-runtime.checklib
-
Library
rocq-runtime.clib
-
Library
rocq-runtime.config
-
Library
rocq-runtime.coqargs
-
Library
rocq-runtime.coqworkmgrapi
-
Library
rocq-runtime.debugger_support
-
Library
rocq-runtime.dev
-
Library
rocq-runtime.engine
-
Library
rocq-runtime.interp
-
Library
rocq-runtime.kernel
-
Library
rocq-runtime.lib
-
Library
rocq-runtime.library
-
Library
rocq-runtime.perf
-
Library
rocq-runtime.pretyping
-
Library
rocq-runtime.printing
-
Library
rocq-runtime.proofs
-
Library
rocq-runtime.rocqshim
-
Library
rocq-runtime.stm
-
Library
rocq-runtime.sysinit
-
Library
rocq-runtime.tactics
-
Library
rocq-runtime.toplevel
-
Library
rocq-runtime.vernac
-
Library
rocq-runtime.vm
-
Library
rtauto_plugin
-
Library
ssreflect_plugin
-
Library
ssrmatching_plugin
-
Library
tauto_plugin
-
Library
tuto0_plugin
-
Library
tuto1_plugin
-
Library
tuto2_plugin
-
Library
tuto3_plugin
-
-
btauto_plugin
-
byte_config
-
cc_core_plugin
-
cc_plugin
-
derive_plugin
-
firstorder_core_plugin
-
firstorder_plugin
-
ltac2_ltac1_plugin
-
ltac_plugin
-
micromega_core_plugin
-
nsatz_core_plugin
-
nsatz_plugin
-
number_string_notation_plugin
-
ring_plugin
-
rocq-runtime.clib
-
rocq-runtime.config
-
rocq-runtime.coqargs
-
rocq-runtime.coqdeplib
-
rocq-runtime.coqworkmgrapi
-
rocq-runtime.debugger_support
-
rocq-runtime.dev
-
rocq-runtime.gramlib
-
rocq-runtime.kernel
-
rocq-runtime.library
-
rocq-runtime.parsing
-
rocq-runtime.perf
-
rocq-runtime.pretyping
-
rocq-runtime.printing
-
rocq-runtime.proofs
-
rocq-runtime.rocqshim
-
rocq-runtime.sysinit
-
rocq-runtime.tactics
-
rocq-runtime.vernac
-
rocq-runtime.vm
-
rtauto_plugin
-
ssrmatching_plugin
-
tauto_plugin
-
tuto0_plugin
-
tuto2_plugin
-
tuto3_plugin
-
zify_plugin
-
-
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source