Global $n$-compact Validation Engine
Tutorials
Getting Started Examples
Lurch Node REPL
Global Propositional Form
Classes
C
CNFProp
M
signature
M
switchVarSymbol
F
hasCNFform
F
simplify
F
toAlgebraic
F
toArray
F
toEnglish
F
fromLC
F
toCNF
F
toVar
C
TreeIndexer
F
define
F
delete
F
get
F
show
F
update
F
updateAll
C
MathItem
F
get
F
setFocusWhenShown
F
setValue
Modules
M
GlobalValidation
M
isDopplegangerOf
F
cacheFormulaDomainInfo
F
copyEquation
F
diff
F
eq2chain
F
forbiddenWeeny
F
getCaselikeRules
F
getUserPropositions
F
insertInstantiation
F
insertSymmetricEquivalences
F
instantiate
F
instantiateTransitives
F
isBadInstantiation
F
markFlaggedDeclarations
F
matchGivens
F
matchPropositions
F
patternForm
F
processBIHs
F
processCases
F
processChains
F
processDomains
F
processEquations
F
reverseEquation
F
splitChains
F
splitEquations
F
tidyProperNames
F
upgradeChains
F
validate
M
Interpretation
M
systemConstants
F
addSystemDeclarations
F
assignProperNames
F
canonicalizeBindings
F
interpret
F
markDeclaredSymbols
F
moveDeclaresToTop
F
processBindings
F
processDeclarationBodies
F
processLetEnvironments
F
processRules
F
processTheorems
F
removeTrailingGivens
F
renameBindings
F
replaceBindings
F
splitConclusions
M
Lode
F
list
M
MathLive
M
inputFormats
M
outputFormats
M
stylesheet
F
getConverter
M
Parsing
M
arithmeticToCAS
M
isNegationOfArithmetic
F
processShorthands
F
makeParser
F
numericToCAS
F
parseLines
F
partition
M
Reporting
M
Utilities
M
isOnScreen
F
appURL
F
copyWithoutPrototype
F
editorForNode
F
escapeHTML
F
loadScript
F
onlyBefore
F
removeScriptTags
F
simpleHTMLTable
F
checkExtension
F
checkFolder
F
commonInitialSlice
F
hex2rgb
F
indent
F
lineNum
F
rgb2hex
F
subscript
F
tab
F
timer
M
z3
Namespaces
N
Extensions
F
Declaration#allProps
F
Declaration#letsInScope
F
Declaration#lookup
F
Declaration#prop
F
Environment#catalog
F
Environment#cnf
F
Environment#letInferences
F
Environment#scopes
F
Expression#allProps
F
Expression#lookup
F
Expression#prop
F
LogicConcept#Insts
F
LogicConcept#Parts
F
LogicConcept#attributes
F
LogicConcept#bindings
F
LogicConcept#chains
F
LogicConcept#declarations
F
LogicConcept#descendantsSatisfyingIterator
F
LogicConcept#environments
F
LogicConcept#equations
F
LogicConcept#find
F
LogicConcept#forSomes
F
LogicConcept#formulas
F
LogicConcept#getDeclares
F
LogicConcept#getRules
F
LogicConcept#getTheorems
F
LogicConcept#insertAfter
F
LogicConcept#insertBefore
F
LogicConcept#isAChain
F
LogicConcept#isAComment
F
LogicConcept#isADeclaration
F
LogicConcept#isAForSome
F
LogicConcept#isALet
F
LogicConcept#isALetEnvironment
F
LogicConcept#isAProposition
F
LogicConcept#isAStatement
F
LogicConcept#isAnEquation
F
LogicConcept#letAncestors
F
LogicConcept#lets
F
LogicConcept#mentions
F
LogicConcept#metavars
F
LogicConcept#negate
F
LogicConcept#propositions
F
LogicConcept#results
F
LogicConcept#root
F
LogicConcept#setResult
F
LogicConcept#slice
F
LogicConcept#some
F
LogicConcept#statements
F
LogicConcept#symbols
F
LogicConcept#toAlgebraic
F
LogicConcept#toEnglish
F
LogicConcept#toNice
F
LogicConcept#toggleGiven
F
LurchSymbol#properName
F
LurchSymbol#rename
Globals
M
LurchOptions
M
addIndex
M
addLurchIndices
F
compileSingleTest
F
computeChainResult
F
elapsedTime
F
loadAcidTests
F
loadStudentTests
F
loadTest
F
putdownSymbolText
M
runParserTests
F
runTests
F
safeExecute
Module
z3
Lurch integration with z3
Source
z3.js
, line 1