中間表現、未整理

翻訳：

• let → we_have
• := → by_using, because_of
• return → we_conclude, we_showed
• suffice

let/return式

let x1: A1 := τ1
let x2: A2 := τ2
‥‥
return α: C
end

別な書き方：

we_have x1: A1 by_using τ1
we_have x2: A2 by_using τ2
‥‥
we_conclude C by_using α
end

return/where式

return α: C using x1: A1, x2: A2, ‥‥
where x1: A1 := τ1
where x2: A2 := τ2
‥‥
end

別な書き方：

suffice x1: A1, x2: A2, ‥‥ 
to_show C because_of α

キーワード列挙、順不同：

1. ensures ＝ implements
2. return α: A providing x: X ＝ suffice x:X to_show A because_of α
3. within Γ return α : A または within Γ assert α : A
4. let ... and_also ...
5. where ... and_also ...
6. let ＝ we_have
7. := ＝ by_using, because_of
8. define ＝ function ＝ theorem
9. { ＝ proof, } ＝ end

return と assert の違い。

• return α: A は、計算結果αに注目している。型Aは添え物、省略していい。
• assert α: A は、型Aであることに注目している。場合により、αを省略していい。そのときは、αが存在するという存在のメタ命題を主張している。
• ensure A は、assert _: A と同義。アンダースコアはdon't care marker。