lean-ja / lean-ja/lean-by-example
TSyntax には declare_syntax_cat で宣言したカテゴリを入れることができるという例
Open
Nobody has claimed this yet.
要調査
- Dominant language
- Lean
- Stars
- 188
- Forks
- 15
- Avg merge
- 9h 8m
- Merged PRs (30d)
- 6
Description
メタプロ本より。
declare_syntax_cat arith
syntax num : arith
syntax arith "-" arith : arith
syntax arith "+" arith : arith
syntax "(" arith ")" : arith
partial def denoteArith : TSyntax `arith → Nat
| `(arith| $x:num) => x.getNat
| `(arith| $x:arith + $y:arith) => denoteArith x + denoteArith y
| `(arith| $x:arith - $y:arith) => denoteArith x - denoteArith y
| `(arith| ($x:arith)) => denoteArith x
| _ => 0
-- You can ignore Elab.TermElabM, what is important for us is that it allows
-- us to use the ``(arith| (12 + 3) - 4)` notation to construct `Syntax`
-- instead of only being able to match on it like this.
def test : Elab.TermElabM Nat := do
let stx ← `(arith| (12 + 3) - 4)
pure (denoteArith stx)
/- info: 11 -/
#eval test
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
No file or test is named. Start by locating the appropriate Lean example or syntax-documentation section, then adapt the supplied declare_syntax_cat and TSyntax example there. Done means the example is included in the documentation and demonstrates the stated evaluation result of 11.
Written by the indexing model from the issue text.
Assessment
- Domain
- documentation
- Issue type
- Documentation
- Difficulty
- 2/5
- Estimated time
- 1-3 hours
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 42/100