package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.15.1.tar.gz
sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2
doc/ltac_plugin/Ltac_plugin/Pltac/index.html
Module Ltac_plugin.Pltac
Source
Ltac parsing entries
Source
val constr_may_eval :
(Constrexpr.constr_expr,
Libnames.qualid Constrexpr.or_by_notation,
Constrexpr.constr_expr)
Genredexpr.may_eval
Pcoq.Entry.t
Source
val destruction_arg :
Constrexpr.constr_expr Tactypes.with_bindings Tactics.destruction_arg
Pcoq.Entry.t
Source
val simple_intropattern :
Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t Pcoq.Entry.t
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>