Skip to content
This repository has been archived by the owner on Aug 14, 2024. It is now read-only.
/ lyre Public archive

๐ŸŽผ | An incomplete LALR(1) DSL for Lean, intended to compile to an LR table but not yet to Lean code.

Notifications You must be signed in to change notification settings

algebraic-dev/lyre

Folders and files

NameName
Last commit message
Last commit date

Latest commit

7ca6a07 ยท Jun 15, 2022

History

6 Commits
Jun 15, 2022
Jun 12, 2022
Jun 15, 2022
Jun 15, 2022
Jun 12, 2022
Jun 12, 2022

Repository files navigation

Lyre

Incomplete LALR(1) DSL for Lean (that compiles to a LR Table but does not compile to lean code lol)

import Lyre.Grammar
import Lyre.LR1
import Lyre.DSL
open DSL

grammar myGrammar where

  start s { String }

  token x      : { "a" }
  token star   : { "v" }
  token eq     : { "c" }

  rule s
    :            { Int }
    | s s star   { d }
    | s s x      { x }
    | x          { e }

About

๐ŸŽผ | An incomplete LALR(1) DSL for Lean, intended to compile to an LR table but not yet to Lean code.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages