`code_pred`ってなにやってるんだ？

[2222-42]

why

inductive_casesと同じくらい、おまじない的に使っている、code_predについて詳しく知らない。

その定義も、用法も。

what

• 調べる。
• Theory Sec_Typingを読み直す。

[2222-42]

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-October/msg00229.html

[2222-42]

The code_pred command takes the name of the inductive predicate and
then you put a period to discharge a trivial correctness proof. The compiler
infers possible modes for the predicate and produces the derived code equations. Modes annotate which (parts of the) arguments are to be taken as
input, and which output. Modes are similar to types, but use the notation i
for input and o for output
https://isabelle.in.tum.de/doc/codegen.pdf

[2222-42]

コマンドでの実行を可能にしている？