Awesome Lean / Libraries
21Metaprogramming & DSLs
11 entries
- QqIntuitive, type-safe expression quotations.leanprover-community/quote4
- ThymeTyped, staged metaprogramming with dependent types and reasoning about metaprograms.frangio/thyme
- LeanductionGenerates usable induction principles for nested inductive types.arthur-adjedj/Leanduction
- MutualInductionMutual induction tactic.ionathanch/MutualInduction
- QPF(Co)datatype package built on quotients of polynomial functors.alexkeizer/QPFTypes
- CoinductiveLibrary for coinductive types built on polynomial functors, used to define interaction trees.ISTA-PLV/coinductive
- leansesLenses with custom notation.VCA-EPFL/leanses
- lean-substSubstitution library inspired by Autosubst.amarmaduke/lean-subst
- HexLuthorHex color literal syntax with inline VS Code preview.alok/HexLuthor
- ImperiaAlternative
donotation for imperative code over non-monadic types (experimental).tydeu/imperia - LeanBitsyntaxErlang-style
<<...>>bit syntax for building and matchingBitVecvalues (experimental).palladin/lean-bitsyntax