lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
1024" x-on:close-sidebar="sidebar=window.innerWidth > 1024 && true">
package lambdapi
-
lambdapi.tool
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type loc = Lexing.position * Lexing.position
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 |
ON THIS PAGE
No table of contents