package coq-flocq
  A formalization of floating-point arithmetic for the Coq system
Install
Dune Dependency
Authors
Maintainers
Sources
  
    
      flocq-4.2.1.tar.gz
    
    
        
    
  
  
  
    
  
        sha512=73a93f1b7d7b0d1ad731a87c1fbf80d363cc479259059618170d488eb7ff2e101d4e3adf850796b3d20455c94ba093ad39d9ef80e3e03e53b20f6e9df1886736
    
    
  Description
Dependencies (3)
- 
  
    conf-clang
  
  
    build
- 
  
    conf-g++
  
  
    build
- 
  
    coq
  
  
    >= "8.15"
Dev Dependencies (1)
- 
  
    conf-autoconf
  
  
    build & dev
Used by (18)
- 
  
    coq-compcert
  
  
    >= "3.7~coq-platform" & < "3.7" | >= "3.11"
- 
  
    coq-compcert-32
  
  
    >= "3.11"
- 
  
    coq-compcert-64
  
  
    < "3.7"
- 
  
    coq-flocq-quickchick
  
  
    >= "1.0.1"
- 
  
    coq-gappa
  
  
    >= "1.4.0" & < "1.4.4" | >= "1.5.0"
- 
  
    coq-interval
  
  
    >= "3.4.0" & < "4.0.0" | >= "4.3.0"
- 
  
    coq-libvalidsdp
  
  
    >= "0.6.0"
- coq-num-analysis
- 
  
    coq-qcert
  
  
    = "1.0.9"
- coq-validsdp
- coq-vcfloat
- coq-vellvm
- 
  
    coq-vst
  
  
    >= "2.6"
- coq-vst-32
- coq-vst-64
- coq-vst-lib
- rocq-num-analysis-lebesgue
- rocq-vellvm
Conflicts
None
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
On This Page