package coq-lean-import
  Plugin allowing Coq to import Lean exported files
Install
Dune Dependency
Authors
Maintainers
Sources
  
    
      v9.0-lean3+alpha.tar.gz
    
    
        
    
  
  
  
    
  
        sha512=2f49766d0b667d897b5a62b4806db129967c717ad0a15d484da6c29ee77e85a918188ffa4cb0372c320ea6563df1a5e8273f9d2e7c8745c220c5aa2b3f7bf9fa
    
    
  Description
Plugin allowing Coq to import Lean exported files.
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
On This Page