package coq-text2tac

  1. Overview
  2. Homepage
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

Dependencies (1)

  1. coq-tactician-api = "15.0+8.11"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover