lean-ja/lean-by-example

`[computed_field]` 属性とは何か

Opened this issue · 1 comments

Seasawher commented

Name の定義に出現する：

inductive Name where
  /-- The "anonymous" name. -/
  | anonymous : Name
  /--
  A string name. The name `Lean.Meta.run` is represented at
  -/
  | str (pre : Name) (str : String)
  /--
  A numerical name. This kind of name is used, for example, to create hierarchical names for
  free variables and metavariables. The identifier `_uniq.231` is represented as
  -/
  | num (pre : Name) (i : Nat)
with
  /-- A hash function for names, which is stored inside the name itself as a
  computed field. -/
  @[computed_field] hash : Name → UInt64
    | .anonymous => .ofNatCore 1723 (by decide)
    | .str p s => mixHash p.hash s.hash
    | .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide)))