- 主語 we
- 動詞 declare, define, approve〈アプルーブ〉
- 副動詞 request, respond
- 名前の修飾語 type, function
- typeへの副修飾語 logical, type-param, prop-param
- functionへの副修飾語 section, bundle, type-velued, prop-valued, partial
- 終止語 end
- その他 applying, using, namespace, within
仕様句内のキーワード
- for
- where
- when
- let
- returns type （ニ語組み合わせ）
- says prop （略語）
短縮語・略語
- prop ＝ logical type
- prop-valued ＝ logical-type-valued
- theorem ＝ prop-valued function ＝ logical-type-valued function
- instance ＝ section function
- family ＝ type-valued function
- predicate ＝ logical-type-valued function ＝ prop-valued function
- logical family ＝ logical-type-valued function ＝ predicate
- says prop ＝ returns logical type
$`\newcommand{\T}[1]{\text{#1}}
\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\In}{\text{ in }}
\newcommand{\Imp}{\mathop{ =\!\!\triangleright }}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\PiTy}{\leadsto}
\newcommand{\LL}{\big\langle}
\newcommand{\LR}{\big\rangle}
\newcommand{\hyp}{\text{－} } % used
\require{color} % Using
\newcommand{\NN}[1]{ \textcolor{orange}{\text{#1}} } % New Name
\newcommand{\NX}[1]{ \textcolor{orange}{#1} } % New EXpression
\newcommand{\T}[1]{\text{#1} }
`$
$`\T{we define function } \NN{f1}\\
\quad \T{for }x:\in {\bf R}, y:\in {\bf R}\\
\quad \T{returns type }{\bf R}\\
\T{applying}\\
\quad x^2 + y^2\\
\T{end}\\
\:\\
\T{we declaree partial function } \NN{f2}\\
\quad \T{for }x:\in {\bf N}, y:\in {\bf N}\\
\quad \T{when }x \le y\\
\quad \T{returns type }{\bf N}\\
\T{end}\\
\:\\
\T{we define partial function } \T{f2}\\
\quad \T{for }x, y\\
\T{applying}\\
\quad y - x\\
\T{end}\\
\:\\
\T{using }{\bf R}_{\le 0}\\
\T{we declare theorem } \NN{t1}\\
\quad \T{for }x:\in {\bf R}, y:\in {\bf R}\\
\quad \T{says prop } x\in {\bf R}_{\le 0} \land y\in {\bf R}_{\le 0} \Imp x + y \in {\bf R}_{\ge 0}\\
\T{end}\\
\:\\
\T{we approve theorem } \T{t1} \T{ end}
`$
型構成子
| $`\text{non-logical POV}`$ | $`\T{logical POV}`$ |
|---|---|
| $`{\bf Type}`$ | $`{\bf Prop}`$ |
| $`\times`$ | $`\land`$ |
| $`+`$ | $`\lor`$ |
| $`{\bf 1}`$ | $`\top`$ |
| $`{\bf 0}`$ | $`\bot`$ |
| $`\diamond\!\!\to`$ | $`\Imp`$ |
| $`\sum,\: \ltimes`$ | $`\exists`$ |
| $`\prod,\: \diamond\!\!\leadsto`$ | $`\forall`$ |
関係
| $`\text{non-logical type}`$ | $`\T{logical type}`$ |
|---|---|
| $`\mrm{Crush}(X) = \mrm{Crush}(Y)`$ | $`X \equiv Y`$ |
| $`\langle X \to Y\rangle \ne {\bf 0}`$ | $`X \sqsubseteq Y`$ |
