6.10. Type Ascription

Type ascriptions は項の型を明示的に注釈します。これは Lean に対して、項に期待される型を提供する方法です。この型は項の文脈から予想される型と definitionally equal でなければなりません。type ascription は単にプログラムを文書化する以外にも役立ちます：

  • プログラムのテキストには、項の型を導くのに十分な情報がない場合があります。ascription はそのような型を提供する方法の1つです。

  • 推論された型は項に望まれた型ではないかもしれません。

  • 項の期待される型は coercions の挿入を推進するために使用され、ascription はどこに強制が挿入されるかを制御する方法の1つです。

syntaxPostfix Type Ascriptions

Type ascriptions はカッコで囲まなければなりません。これは最初の項の型が2番目の項であることを示します。

term ::= ...
    | Type ascription notation: `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
An empty type ascription `(e :)` elaborates `e` without the expected type.
This is occasionally useful when Lean's heuristics for filling arguments from the expected type
do not yield the right result.
(term : term)

タクティク証明や Lean.Parser.Term.do : termdo ブロックのように、type ascription を必要とする項が長い場合、必須の括弧を持ち後置される type ascription は読みにくい場合があります。さらに、証明と Lean.Parser.Term.do : termdo ブロックの両方で項の型はその解釈に不可欠です。このような場合、前置する方が読みやすくなります。

syntaxPrefix Type Ascriptions
term ::= ...
    | show term from term

Lean.Parser.Term.show : termshow の本体中の項が証明である場合、 Lean.Parser.Term.show : termfrom は省略することができます。

term ::= ...
    | show term by A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
Delimiter-free indentation is determined by the *first* tactic of the sequence. tacticSeq
証明に対する ascription 文

この例では、目的の命題がわからないため、タクティクによる証明を実行できません。先に実行されたタクティクによって、命題はタクティクが証明できるものに自動的に絞り込まれます。しかし、デフォルトのケースはそれを間違って埋めてしまい、証明は失敗します。

example (n : Nat) := n:Nat⊢ HEq 0 n ⊢ HEq 0 0n✝:Nata✝:HEq 0 n✝⊢ HEq 0 (n✝ + 1) next ⊢ HEq 0 0 All goals completed! 🐙 next n' ih n':Natih:HEq 0 n'⊢ HEq 0 (n' + 1) n':Natih:HEq 0 n'⊢ HEq 0 n'.succ rewrite [n':Natih:HEq 0 n'⊢ HEq 0 n'.succ] rfl 
tactic 'rewrite' failed, equality or iff proof expected
  HEq 0 n'
n' : Nat
ih : HEq 0 n'
⊢ HEq 0 n'.succ

Lean.Parser.Term.show : termshow による前置された ascription を、証明される命題を提供するために使用できます。これはローカル定義として追加すると不便な構文コンテキストで役立ちます。

example (n : Nat) := show 0 + n = n by ⊢ 0 + 0 = 0n✝:Nata✝:0 + n✝ = n✝⊢ 0 + (n✝ + 1) = n✝ + 1 next ⊢ 0 + 0 = 0 All goals completed! 🐙 next n' ih n':Natih:0 + n' = n'⊢ 0 + (n' + 1) = n' + 1 n':Natih:Nat.add 0 n' = n'⊢ (Nat.add 0 n').succ = n'.succ rewrite [n':Natih:Nat.add 0 n' = n'⊢ n'.succ = n'.succ] All goals completed! 🐙
Lean.Parser.Term.do : termdo ブロックに対する type ascription

この例では、 Pure インスタンスを統合するのに十分な型情報がありません。

example := do typeclass instance problem is stuck, it is often due to metavariables Pure ?m.75return 5 
typeclass instance problem is stuck, it is often due to metavariables
  Pure ?m.75

Lean.Parser.Term.show : termshow による前置された ascription と ホール を併用することで、モナドを示すことができます。 デフォルトの OfNat _ 5 インスタンスは、 Nat でホールを埋めるのに十分な型情報を提供します。

example := show StateM String _ from do return 5