package lambdapi
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
  Proof assistant for the λΠ-calculus modulo rewriting
Install
    
    dune-project
 Dependency
Authors
Maintainers
Sources
  
    
      lambdapi-2.3.0.tbz
    
    
        
    
  
  
  
    
  
  
    
  
        sha256=9b13c3121ef87cf4d3311a8a1db43db4be7f0e5e2a702fdaff04a3b3c432cb31
    
    
  sha512=81e0760ca77cb862a5bdb8927aa37faf7141c4e2484a8163dad0a3eaa21cc691acb5f72279c78588c085f53dde4bd35186346378feac0ab55ac06a679cf2e60f
    
    
  doc/lambdapi.parsing/Parsing/DkTokens/index.html
Module Parsing.DkTokensSource
Dedukti source file parsing/tokens.ml.
Source
type token = - | UNDERSCORE of loc
- | TYPE of loc
- | KW_DEF of loc
- | KW_DEFAC of loc
- | KW_DEFACU of loc
- | KW_THM of loc
- | KW_INJ of loc
- | KW_PRV of loc
- | RIGHTSQU
- | RIGHTPAR
- | RIGHTBRA
- | QID of loc * DkBasic.mident * DkBasic.ident
- | NAME of loc * DkBasic.mident
- | REQUIRE of loc * DkBasic.mident
- | LONGARROW
- | LEFTSQU
- | LEFTPAR
- | LEFTBRA
- | ID of loc * DkBasic.ident
- | FATARROW
- | EOF
- | DOT
- | DEF
- | COMMA
- | COLON
- | EQUAL
- | ARROW
- | EVAL of loc
- | INFER of loc
- | CHECK of loc
- | ASSERT of loc
- | CHECKNOT of loc
- | ASSERTNOT of loc
- | PRINT of loc
- | GDT of loc
- | STRING of string
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >