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
On This Page