私はソフトウェア基盤に取り組んでおり、現在は教会の数字に関する演習を行っています. 自然数の型シグネチャは次のとおりです。
Definition nat := forall X : Type, (X -> X) -> X -> X.
succtypeの関数を定義しましたnat -> nat。次のように加算関数を定義したいと思います。
Definition plus (n m : nat) : nat := n nat succ m.
ただし、次のエラー メッセージが表示されます。
Error: Universe inconsistency.
このエラー メッセージの実際の意味は何ですか?