Ryusei’s Notes (a.k.a. M59のブログ)

表明から証明へ (3) headを証明する HaskellのPrelude.headとは異なり、IdrisのPrelude.List.headは、引数にコンスセルである証明をとるので、全域函数になっている。Idrisのシステムでは次のように、%assert_total宣言によって、全域函数であることが「表明」されている。 %assert_total head : (l : List a) -> (isCons …