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.5.0.tbz
    
    
        
    
  
  
  
    
  
  
    
  
        sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
    
    
  sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704
    
    
  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)"
  >