6.3　predicate の定義

　まず，predicate の定義について説明します．例えば，k, l を自然数として，いま，k は l の因子である，という定義をしたいとします．これは predicate です．k is factor of l ，このような定義をしたいとします．これは二項演算子の様な形をしてますけれども，k, l と2つ変数を持っているわけです．この場合どうやって定義を書くかというと，

　　　definition
　　　let k,l be Nat;
　　　pred k is_factor_of l
　　　means
　　　:FACTOR:
　　　ex t being Nat st l=k·t


となります．let k,l be Nat の Nat は，k, l の Mode が自然数であることをあらわしています．:FACTOR: はラベルで，後で引用するときにこのラベルを使います．定義のなかのラベルは両側をコロンではさみます．そして，これは abstract file をここから抜きだして作るときには，def に数字がついたものに変えられます．ふつうの定理のラベルは単なる数字に変えられます．また　k·t の · はかけ算です．
　これで，k is_factor_of l という predicate とは ex t being Nat st l=k·t ということを意味しています．