Definition of lexer RLexer, which is a subclass of CharScanner.

/** Lexer nextToken rule:
 *  The lexer nextToken rule is synthesized from all of the user-defined
 *  lexer rules.  It logically consists of one big alternative block with
 *  each user-defined rule being an alternative.
 */
mWORD_SEQUENCE 
|	mWS 
|	mSL_COMMENT 
|	mML_COMMENT 
|	mDOT 
|	mNUMERIC_LITERAL 
|	mCHARACTER_LITERAL 
|	mCOMMA 
|	mLPAREN 
|	mRPAREN 
|	mLBRACE 
|	mRBRACE 
|	mDBL_LBRACE 
|	mDBL_RBRACE 
|	mLSQBRACK 
|	mRSQBRACK 
|	mHASH 
|	mCARAT 
|	mPLUS 
|	mMINUS 
|	mAMPERSAND 
|	mMULTIPLY 
|	mDIVIDE 
|	mEXP 
|	mRANGE 
|	mNOT_EQL 
|	mGT_EQL 
|	mLT_EQL 
|	mEQL 
|	mLT 
|	mGT 
|	mLL 
|	mGG 
|	mFUNCARROW 
|	mCOLON 
|	mSEMICOLON 
|	mSWAP_OP 
|	mASSIGN_OP 
|	mBAR 
|	mDBL_BAR 
|	mDQUOTE 
|	mTILDE 
|	mSTRING_LITERAL 
|	mFREE_OPERATOR 
mWORD_SEQUENCE
	:	mTHEORY 
	|	mPROOFS_FOR 
	|	mFORALL 
	|	mEXISTS_UNIQUE 
	|	mEXISTS 
	|	mST 
	|	mALTERS 
	|	mCLEARS 
	|	mEVALUATES 
	|	mPRESERVES 
	|	mREPLACES 
	|	mRESTORES 
	|	mUPDATES 
	|	mREASSIGNS 
	|	mENHANCED_BY 
	|	mREALIZED_BY 
	|	mMODELED 
	|	mREPRESENTED 
	|	mPROCEDURE 
	|	mRECURSIVE_PROCEDURE 
	|	mOPERATION 
	|	mAUX_OPERATION 
	|	mVARS 
	|	mVAR 
	|	mAUXVARS 
	|	mAUXVAR 
	|	mIMPLICIT_DEF 
	|	mINDUCTIVE_DEF 
	|	mDEFINITION 
	|	mDEFINES 
	|	mLOCAL_MATH_TYPE 
	|	mMATH_TYPE 
	|	mMATH_SUBTYPE 
	|	mTYPE_FAMILY 
	|	mTYPE 
	|	mCONSTRAINTS 
	|	mCONSTRAINT 
	|	mCORR 
	|	mCONVENTIONS 
	|	mCONVENTION 
	|	mBY 
	|	mPROPERTY 
	|	mPOWERSET 
	|	mEXCLUDED_MIDDLE 
	|	mMODUS_PONENS 
	|	mAND_RULE 
	|	mALTERNATIVE_ELIMINATION 
	|	mCOMMON_CONCLUSION 
	|	mREDUCTIO_AD_ABSURDUM 
	|	mUNIVERSAL_GENERALIZATION 
	|	mEXISTENTIAL_GENERALIZATION 
	|	mOR_RULE 
	|	mCONJUNCT_ELIMINATION 
	|	mQUANTIFIER_DISTRIBUTION 
	|	mUNIVERSAL_INSTANTIATION 
	|	mEXISTENTIAL_INSTANTIATION 
	|	mIF 
	|	mIDENTIFIER 
	;

protected mTHEORY
	:	"Theory" 
	|	"Precis" 
	;

mWS
	:	(	' ' 
		|	'\t' 
		|	'\f' 
		|	(	"\r\n" 
			|	'\r' 
			|	'\n' 
			) 
			
		) 
		
	;

protected mPROOFS_FOR
	:	"Proofs_for" 
	|	"Proof" ( mWS )+ 
		(	"unit" 
		|	"Unit" 
		) 
	;

protected mFORALL
	:	(	"For" 
		|	"for" 
		) 
		( mWS )+ "all" 
	;

protected mEXISTS_UNIQUE
	:	(	"There" 
		|	"there" 
		) 
		( mWS )+ "exists" ( mWS )+ "unique" 
	;

protected mEXISTS
	:	(	"There" 
		|	"there" 
		) 
		( mWS )+ "exists" 
	;

protected mST
	:	"such" ( mWS )+ "that" 
	;

protected mALTERS
	:	"alters" 
	|	"alt" 
	;

protected mCLEARS
	:	"clears" 
	|	"clr" 
	;

protected mEVALUATES
	:	"evaluates" 
	|	"eval" 
	;

protected mPRESERVES
	:	"preserves" 
	|	"pres" 
	;

protected mREPLACES
	:	"replaces" 
	|	"rpl" 
	;

protected mRESTORES
	:	"restores" 
	|	"rest" 
	;

protected mUPDATES
	:	"updates" 
	|	"upd" 
	;

protected mREASSIGNS
	:	"reassigns" 
	|	"rea" 
	;

protected mENHANCED_BY
	:	"enhanced" ( mWS )+ "by" 
	;

protected mREALIZED_BY
	:	"realized" ( mWS )+ "by" 
	;

protected mMODELED
	:	"is" ( mWS )+ "modeled" ( mWS )+ "by" 
	;

protected mREPRESENTED
	:	"is" ( mWS )+ "represented" ( mWS )+ "by" 
	;

protected mPROCEDURE
	:	"Procedure" 
	|	"Proc" 
	;

protected mRECURSIVE_PROCEDURE
	:	"Recursive" ( mWS )+ 
		(	"Procedure" 
		|	"Proc" 
		) 
	|	"recursive" ( mWS )+ 
		(	"Procedure" 
		|	"Proc" 
		) 
	;

protected mOPERATION
	:	"Operation" 
	|	"Oper" 
	|	"operation" 
	|	"oper" 
	;

protected mAUX_OPERATION
	:	"Auxiliary" ( mWS )+ 
		(	"Operation" 
		|	"Oper" 
		) 
	|	"Aux" ( mWS )+ 
		(	"Operation" 
		|	"Oper" 
		) 
	;

protected mVARS
	:	"Variables" 
	|	"Vars" 
	;

protected mVAR
	:	"Variable" 
	|	"Var" 
	;

protected mAUXVARS
	:	"Aux_Vars" 
	|	"Aux_Variables" 
	;

protected mAUXVAR
	:	"Aux_Var" 
	|	"Aux_Variable" 
	;

protected mIMPLICIT_DEF
	:	"Implicit" ( mWS )+ mDEFINITION 
	;

protected mINDUCTIVE_DEF
	:	"Inductive" ( mWS )+ mDEFINITION 
	;

protected mDEFINITION
	:	"Definition" 
	|	"Def" 
	|	"definition" 
	|	"def" 
	;

protected mDEFINES
	:	"Defines" 
	|	"defines" 
	;

protected mLOCAL_MATH_TYPE
	:	"Local" ( mWS )+ "Math" ( mWS )+ "Type" 
	;

protected mMATH_TYPE
	:	"Math" ( mWS )+ "Type" 
	;

protected mMATH_SUBTYPE
	:	"Math" ( mWS )+ "Subtype" ( mWS )+ "Theorem" 
	;

protected mTYPE_FAMILY
	:	"Type" ( mWS )+ "Family" 
	|	"Type_Family" 
	|	"Family" 
	;

protected mTYPE
	:	"Type" 
	|	"type" 
	;

protected mCONSTRAINTS
	:	"Constraints" 
	|	"constraints" 
	;

protected mCONSTRAINT
	:	"Constraint" 
	|	"constraint" 
	;

protected mCORR
	:	"Correspondence" 
	|	"correspondence" 
	;

protected mCONVENTIONS
	:	"Conventions" 
	|	"conventions" 
	;

protected mCONVENTION
	:	"Convention" 
	|	"convention" 
	;

protected mBY
	:	"By" 
	|	"by" 
	;

protected mPROPERTY
	:	"Property" 
	|	"Pty" 
	;

protected mPOWERSET
	:	"Powerset" 
	|	"powerset" 
	;

protected mEXCLUDED_MIDDLE
	:	"excluded" ( mWS )+ "middle" 
	;

protected mMODUS_PONENS
	:	"modus" ( mWS )+ "ponens" 
	;

protected mAND_RULE
	:	"and" ( mWS )+ "rule" 
	;

protected mALTERNATIVE_ELIMINATION
	:	"alternative" ( mWS )+ "elimination" 
	;

protected mCOMMON_CONCLUSION
	:	"common" ( mWS )+ "conclusion" 
	;

protected mREDUCTIO_AD_ABSURDUM
	:	"reductio" ( mWS )+ "ad" ( mWS )+ "absurdum" 
	;

protected mUNIVERSAL_GENERALIZATION
	:	"universal" ( mWS )+ "generalization" 
	;

protected mEXISTENTIAL_GENERALIZATION
	:	"existential" ( mWS )+ "generalization" 
	;

protected mOR_RULE
	:	"or" ( mWS )+ "rule" 
	;

protected mCONJUNCT_ELIMINATION
	:	"conjunct" ( mWS )+ "elimination" 
	;

protected mQUANTIFIER_DISTRIBUTION
	:	"quantifier" ( mWS )+ "distribution" 
	;

protected mUNIVERSAL_INSTANTIATION
	:	"universal" ( mWS )+ "instantiation" 
	;

protected mEXISTENTIAL_INSTANTIATION
	:	"existential" ( mWS )+ "instantiation" 
	;

protected mIF
	:	"If" 
	|	"if" 
	;

protected mIDENTIFIER
	:	mLETTER ( mALPHABETIC )* 
	;

mSL_COMMENT
	:	"--" ( ~'\n' )* '\n' 
	;

mML_COMMENT
	:	"(*" 
		(	'*' 
		|	'\n' 
		|	(	'*' 
			|	'\n' 
			) 
		)* 
		"*)" 
	;

protected mLETTER
	:	(				'a'..'z' 
		|				'A'..'Z' 
		) 
	;

protected mALPHABETIC
	:	mLETTER 
	|	'_' 
	|	mDIGIT 
	;

protected mDIGIT
	:			'0'..'9' 
	;

protected mDIGITS
	:	( 			'0'..'9' )+ 
	;

protected mREAL
	:	mDIGITS mDOT mDIGITS 
	;

mDOT
	:	'.' 
	;

mNUMERIC_LITERAL
	:	mDIGITS 
	|	mREAL 
	|	mDIGITS 
	;

mCHARACTER_LITERAL
	:	'\'' 
		(	mESC 
		|	~'\'' 
		) 
		'\'' 
	;

protected mESC
	:	'\\' 
		(	'n' 
		|	'r' 
		|	't' 
		|	'b' 
		|	'f' 
		|	'\'' 
		|	'"' 
		|	'\\' 
		) 
	;

mCOMMA
	:	',' 
	;

mLPAREN
	:	'(' 
	;

mRPAREN
	:	')' 
	;

mLBRACE
	:	'{' 
	;

mRBRACE
	:	'}' 
	;

mDBL_LBRACE
	:	"{{" 
	;

mDBL_RBRACE
	:	"}}" 
	;

mLSQBRACK
	:	'[' 
	;

mRSQBRACK
	:	']' 
	;

mHASH
	:	'#' 
	;

mCARAT
	:	'^' 
	;

mPLUS
	:	'+' 
	;

mMINUS
	:	'-' 
	;

mAMPERSAND
	:	'&' 
	;

mMULTIPLY
	:	'*' 
	;

mDIVIDE
	:	'/' 
	;

mEXP
	:	"**" 
	;

mRANGE
	:	".." 
	;

mNOT_EQL
	:	"/=" 
	;

mGT_EQL
	:	">=" 
	;

mLT_EQL
	:	"<=" 
	;

mEQL
	:	'=' 
	;

mLT
	:	'<' 
	;

mGT
	:	'>' 
	;

mLL
	:	"<<" 
	;

mGG
	:	">>" 
	;

mFUNCARROW
	:	"->" 
	;

mCOLON
	:	':' 
	;

mSEMICOLON
	:	';' 
	;

mSWAP_OP
	:	":=:" 
	;

mASSIGN_OP
	:	":=" 
	;

mBAR
	:	'|' 
	;

mDBL_BAR
	:	"||" 
	;

mDQUOTE
	:	'"' 
	;

mTILDE
	:	'~' 
	;

mSTRING_LITERAL
	:	'"' 
		(	mESC 
		|	(	'"' 
			|	'\\' 
			) 
		)* 
		'"' 
	;

mFREE_OPERATOR
	:	'@' ( mUSABLE )+ 
		(	mDOT ( mUSABLE )+ 
		|	
		) 
	;

protected mUSABLE
	:	(	mALPHABETIC 
		|	mREQUIRED_SYMBOLIC 
		) 
	;

protected mREQUIRED_SYMBOLIC
	:	'~' 
	|	'!' 
	|	'#' 
	|	'$' 
	|	'%' 
	|	'^' 
	|	'&' 
	|	'(' 
	|	')' 
	|	'-' 
	|	'+' 
	|	'*' 
	|	',' 
	|	'/' 
	|	':' 
	|	';' 
	|	'<' 
	|	'=' 
	|	'>' 
	|	'?' 
	|	'@' 
	|	'[' 
	|	'\\' 
	|	']' 
	|	'{' 
	|	'}' 
	;