Interface | Description |
---|---|
LFTerm | |
LFType |
Class | Description |
---|---|
FolTranslator |
Translate Metamath statements and theorems into LF/HOL.
|
LFTerm.LFApply | |
LFTerm.LFConst | |
LFTerm.LFLambda | |
LFTerm.LFVar | |
LFType.LFArrow | |
LFType.LFDed | |
LFType.LFPi | |
LFType.LFTypeConst | |
SetMMConstants | |
SetMMConstants.NotSetMMContext |
Exception | Description |
---|---|
SetMMException |
Thrown when Metamath source file has a non-fatal error such as a syntax
error.
|