This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Syntax definition cfl

Description: Extend class notation with floor (greatest integer) function.

		Ref	Expression
	Assertion	cfl	class \|_