objects

package objects

data structures for the Mizar language following the RelaxNG schema given online

Source: package.scala

Linear Supertypes

AnyRef, Any

Ordering

Alphabetic
By Inheritance

Inherited

objects
AnyRef
Any

Hide All
Show All

Visibility

Public
All

Type Members

class Dictionary extends AnyRef
class Format extends AnyRef
class MizAdjective extends AnyRef
Class for handling Mizar Adjectives
class MizAnd extends MizFormula
trait MizAny extends AnyRef
Trait for all Mizar classes
class MizArticle extends AnyRef
class MizAssume extends MizSkeletonItem
trait MizAttrDef extends MizDefinition
class MizAttrIsDef extends MizIsDef with MizAttrDef
class MizAttrIsRedef extends MizRedefinition with MizIsDef with MizAttrDef
class MizAttrMeansDef extends MizMeansDef with MizAttrDef
class MizAttrMeansRedef extends MizRedefinition with MizMeansDef with MizAttrDef
trait MizAuxiliaryItem extends MizProofItem
class MizBlockThesis extends AnyRef
class MizBy extends MizInference
class MizCCluster extends MizClusterDef
class MizCaseReasoning extends MizProofItem
class MizChoice extends MizTerm
class MizCluster extends AnyRef
Class for handling Mizar Clusters
trait MizClusterDef extends MizAny
class MizConclusion extends MizSkeletonItem
class MizConsider extends MizAuxiliaryItem
class MizConst extends MizTerm
class MizConstFunc extends MizTerm
class MizDefFunc extends MizAuxiliaryItem
class MizDefPred extends MizAuxiliaryItem
class MizDefTheorem extends AnyRef
trait MizDefinition extends MizAny
Definitions with structural info
class MizErr extends MizAny
Class for Parser errors
class MizErrorFrm extends MizFormula
class MizErrorInf extends MizInference
class MizErrorTrm extends MizTerm
class MizExists extends MizFormula
class MizExpMode extends MizDefinition
class MizFCluster extends MizClusterDef
class MizField extends AnyRef
class MizFor extends MizFormula
abstract class MizFormula extends MizAny
Class For Formulas
class MizFraenkel extends MizTerm
class MizFreeVar extends MizTerm
class MizFrom extends MizInference
class MizFunc extends MizTerm
trait MizFuncDef extends MizDefinition
class MizFuncIsDef extends MizIsDef with MizFuncDef
class MizFuncIsRedef extends MizRedefinition with MizIsDef with MizFuncDef
class MizFuncMeansDef extends MizMeansDef with MizFuncDef
class MizFuncMeansRedef extends MizRedefinition with MizMeansDef with MizFuncDef
class MizGiven extends MizSkeletonItem
class MizGlobalRef extends MizRef
class MizInfConst extends MizTerm
trait MizInference extends MizJustification
class MizIs extends MizFormula
trait MizIsDef extends MizDefinition
class MizIt extends MizTerm
class MizIterEquality extends MizJustifiedProposition
class MizIterStep extends AnyRef
trait MizJustification extends MizAny
objects.Reasoning Contains classes for handling Mizar Reasoning
objects.Reasoning Contains classes for handling Mizar Reasoning

Version
09/10/2012
trait MizJustifiedProposition extends MizAuxiliaryItem
class MizJustifiedTheorem extends MizAny
class MizLambdaVar extends MizTerm
class MizLemma extends MizAny
class MizLet extends MizSkeletonItem
class MizLocalRef extends MizRef
class MizLocusVar extends MizTerm
trait MizMeansDef extends MizDefinition
trait MizModeDef extends MizDefinition
class MizModeIsDef extends MizIsDef with MizModeDef
class MizModeIsRedef extends MizRedefinition with MizIsDef with MizModeDef
class MizModeMeansDef extends MizMeansDef with MizModeDef
class MizModeMeansRedef extends MizRedefinition with MizMeansDef with MizModeDef
class MizNot extends MizFormula
Classes for each different kind of Formula available in Mizar
class MizNotation extends MizAny
class MizNow extends MizJustifiedProposition
class MizNum extends MizTerm
class MizPred extends MizFormula
trait MizPredDef extends MizDefinition
class MizPredIsDef extends MizIsDef with MizPredDef
class MizPredIsRedef extends MizRedefinition with MizIsDef with MizPredDef
class MizPredMeansDef extends MizMeansDef with MizPredDef
class MizPredMeansRedef extends MizRedefinition with MizMeansDef with MizPredDef
class MizPrivFunc extends MizTerm
class MizPrivPred extends MizFormula
class MizProof extends MizJustification
trait MizProofItem extends MizAny
class MizPropWithJust extends MizJustifiedProposition
class MizProposition extends MizAny
Class For Propositions
class MizQuaTrm extends MizTerm
class MizRCluster extends MizClusterDef
class MizReasoning extends MizAny
class MizReconsider extends MizAuxiliaryItem
trait MizRedefinition extends MizDefinition
abstract class MizRef extends AnyRef
class MizRegistration extends MizAny
trait MizSchemeArg extends AnyRef
class MizSchemeBlock extends MizAny
class MizSchemeDef extends MizAny
class MizSchemeFunc extends MizTerm
class MizSchemeFuncDecl extends MizSchemeArg
class MizSchemePred extends MizFormula
class MizSchemePredDecl extends MizSchemeArg
class MizSelector extends AnyRef
class MizSet extends MizAuxiliaryItem
trait MizSkeletonItem extends MizProofItem
class MizSkippedProof extends MizJustification
class MizStructDef extends MizAny
class MizTake extends MizSkeletonItem
class MizTakeAsVar extends MizSkeletonItem
abstract class MizTerm extends MizAny
Class For Terms
class MizThesis extends AnyRef
class MizTyp extends AnyRef
Class for handling Mizar Types
class MizVar extends MizTerm
Classes for each different kind of Term available in Mizar
class MizVerum extends MizFormula
class OldXMLDefinition extends MizAny
objects.Definition Contains classes for handling Mizar Definitions
objects.Definition Contains classes for handling Mizar Definitions

Version
10/01/2011
class OldXMLRedefinition extends OldXMLDefinition
case class SourceRef(line: Int, col: Int) extends Product with Serializable
Represents a reference to the .miz source file
Represents a reference to the .miz source file
line
source line
col
source column
case class SourceRegion(start: SourceRef, end: SourceRef) extends Product with Serializable
class Symbol extends AnyRef
class XMLConstructor extends MizAny
trait XMLDefMeaning extends AnyRef
class XMLDefiniens extends AnyRef
class XMLDefinition extends MizAny
class XMLDefinitionBlock extends MizAny
class XMLIsDefMeaning extends XMLDefMeaning
class XMLIsDefiniens extends XMLDefiniens
class XMLMeansDefMeaning extends XMLDefMeaning
class XMLMeansDefiniens extends XMLDefiniens
class XMLPattern extends AnyRef
class XMLRegistrationBlock extends AnyRef

Packages

objects

package objects

Type Members

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

Packages

objects 

package objects

Type Members

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

objects