search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
39 stars 7 forks source link

docString を取得できることを利用する #401

Open Seasawher opened 3 months ago

Seasawher commented 3 months ago

以下のようなコードで，任意の名前の doc string を取得できる これを利用すると，Lean by Example に書けることを増やせそう

import Batteries

open Lean

/--
info: `String` is the type of (UTF-8 encoded) strings.

The compiler overrides the data representation of this type to a byte sequence,
and both `String.utf8ByteSize` and `String.length` are cached and O(1).
-/
#guard_msgs in run_meta do
  let some s ← findDocString? (← getEnv) ``String | failure
  logInfo m!"{s}"
Seasawher commented 2 months ago

docString を取得するコマンドを作ることができる．

import Lean

open Lean Elab.Command in
elab "#doc " x:ident : command => do
  let name ← liftCoreM do realizeGlobalConstNoOverload x
  if let some s ← findDocString? (← getEnv) name then
  logInfo m!"{s}"