Skip to content

Instantly share code, notes, and snippets.

View tydeu's full-sized avatar

Mac Malone tydeu

36 followers · 2 following
  • Lean FRO
  • United States
  • 16:22 (UTC -04:00)
View GitHub Profile
@tydeu
tydeu / CompileParserDescr.lean
Last active July 25, 2022 04:52
Lean 4 example of compiling a ParserDescr to a Parsec parser
/-
Copyright (c) 2021 Mac Malone. All rights reserved.
Released under the MIT license.
Authors: Mac Malone
-/
import Lean.Data.Parsec
import Lean.Elab.ElabRules
import Lean.Parser
@tydeu
tydeu / Cont.hs
Created January 4, 2020 03:08
{-# LANGUAGE RankNTypes #-}
module Cont where
import Data.Coerce
import Data.Function
import Control.Applicative
import Control.Monad
newtype Cont a = Cont { runCont :: forall r. (a -> r) -> r }
@tydeu
tydeu / Main.hs
Created August 17, 2019 19:32
Rebindable Templates
import SpliceI
import SpliceS
main :: IO ()
main = testI >> testS