package rocq-yalla
  Yalla library
Install
Dune Dependency
Authors
Maintainers
Sources
  
    
      v2.0.7.tar.gz
    
    
        
    
  
  
  
    
  
        sha256=400b5edb0740c6d9961206480c92f57ff3b073a40b5d81b0493c4827129b0481
    
    
  Description
YALLA: an LL library for the Rocq Prover Yet Another deep embedding of Linear Logic in Rocq
Tags
keyword:linear logic keyword:metatheory keyword:cut elimination category:Mathematics/Logic/Foundations date:2025-03-26 logpath:YallaPublished: 27 Mar 2025
Dependencies (2)
- rocq-stdlib
- 
  
    rocq-core
  
  
    >= "9.0" & < "9.2~"
Dev Dependencies
None
Used by
None
Conflicts
None
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
On This Page