コンテンツにスキップ

Mizar/定義

出典: フリー教科書『ウィキブックス(Wikibooks)』

vocabularyファイル(*.voc)

記号定義 優先順位1~255(省略すると64)
vocabulary file
記号 定義型 意味 existenceuniqueness
G Structure 構造
以後definitionが必要
M Mode モード
O Functor 関数記号
cluster 統合属性
R Predicate 述語命題
K Left functor bracket 左括弧
L Right functor bracket 右括弧
U Selector 識別子
V Attribute 属性


structureの場合

struct NewFunc(# Syuugo->set,Func->Function #);

~.vocファイルには、以下のように記述する
 GNewFunc
 Usyuugo
 UFunc

証明ファイル中では
 the base of NewFunc(# syuugo,newFunc #)
というように使用する