package coq-hammer-tactics
  Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
  
    
      v1.3.2+9.0.tar.gz
    
    
        
    
  
  
  
    
  
        sha512=2d105d5c229e573841bbc194ca4eb9a688a9f11a38c409f4b6f9a8fd2675a150c72d210f21f05e0fed441013980be0e5d8f22311565d098afe3d479938e811d5
    
    
  Description
Collection of tactics that are used by the hammer for Coq to reconstruct proofs found by automated theorem provers. When the hammer has been successfully applied to a project, only this package needs to be installed; the hammer plugin is not required.
Tags
keyword:automation keyword:hammer keyword:tactics logpath:Hammer.Tactics date:2025-10-04Published: 14 Oct 2025
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
On This Page