lean-ja / lean-ja/lean-by-example
elab_rules 使用例: ハートの数により挙動を変える term elaborator
Open
Nobody has claimed this yet.
メタプログラミング
宣言的コマンド
- Dominant language
- Lean
- Stars
- 188
- Forks
- 15
- Avg merge
- 9h 8m
- Merged PRs (30d)
- 6
Description
import Lean
open Lean Elab Command Term
syntax (name := hi) term " ♥ " " ♥ "? " ♥ "? : term
elab_rules : term
| `( $l ♥ ) => do
let stx : Syntax ← `(Nat.add $l 1)
elabTerm stx (expectedType? := mkConst `Nat)
| `( $l ♥♥ ) => do
let stx : Syntax ← `(Nat.add $l 2)
elabTerm stx (expectedType? := mkConst `Nat)
| `( $l ♥♥♥ ) => do
let stx : Syntax ← `(Nat.add $l 3)
elabTerm stx (expectedType? := mkConst `Nat)
#check_failure ("hello" ♥)
#guard 0 ♥ = 1
#guard 0 ♥ ♥ = 2
#guard 0 ♥ ♥ ♥ = 3
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start by locating where Lean code examples about term elaboration belong in the repository; the issue names no target file or test. Use the supplied elab_rules snippet as the proposed example and confirm the project’s documentation conventions and validation process before adding it.
Written by the indexing model from the issue text.
Assessment
- Domain
- documentation
- Issue type
- Documentation
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 35/100