package coq-hammer

  1. Overview
  2. No Docs
General-purpose automated reasoning hammer tool for Coq

Install

Dune Dependency

github.com Edit opam file Versions (30)

Authors

  1. L
    Lukasz Czajka <lukaszcz@mimuw.edu.pl>
  2. C
    Cezary Kaliszyk <cezary.kaliszyk@uibk.ac.at>

Maintainers

  1. L
    lukaszcz@mimuw.edu.pl

Sources

v1.3.2+8.20.tar.gz
sha512=ec54095d91be602d70c5717f7b9710aca19de8dc02fff97b695aad791912f284438f03c90905ff000ab1e172d1c194cf18ed20f5c33d15edfbd1b85720b38f74

Description

A general-purpose automated reasoning hammer tool for Coq that combines learning from previous proofs with the translation of problems to the logics of automated systems and the reconstruction of successfully found proofs.

Tags

category:Miscellaneous/Coq Extensions keyword:automation keyword:hammer logpath:Hammer.Plugin date:2024-11-15

Published: 15 Nov 2024

Dependencies (5)

  1. coq-hammer-tactics = version
  2. conf-clang build
  3. conf-g++ build
  4. coq >= "8.20" & < "8.21~"
  5. ocaml >= "4.09"

Dev Dependencies

None

Used by (1)

  1. coq-operads

Conflicts

None