package coq-text2tac
Language model that predicts tactics for Tactician
Install
Dune Dependency
Authors
Maintainers
Description
Text2Tac is a language model for synthesizing tactics. It receives the current proof state as a human-readable prompt and “completes” this prompt by synthesizing a tactic.
Published: 11 Jan 2024
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page