Skip to content

Instantly share code, notes, and snippets.

Avatar

Gergő Érdi gergoerdi

View GitHub Profile
View TraverseTerm.idr
traverseTerm : (Applicative f) => (Var vars1 -> f (Term vars2)) -> (Term vars1 -> f (Term vars2))
traverseTerm go (Local idx p) = go (MkVar p)
traverseTerm go (Ref nt x) = pure $ Ref nt x
traverseTerm go (Meta x ts) = Meta x <$> traverse (traverseTerm go) ts
traverseTerm go (Bind x b scope) = Bind x <$> traverse (traverseTerm go) b <*> traverseTerm go' scope
where
go' : Var (x :: vars1) -> f (Term (x :: vars2))
go' (MkVar First) = pure $ Local _ First
go' (MkVar (Later p)) = weaken <$> go (MkVar p)
traverseTerm go (App f e) = App <$> traverseTerm go f <*> traverseTerm go e
View globalrichlist.js
function r(e) {
var n =
[[1.11e11, 0.6819],
[8.12e10, 0.6518],
@gergoerdi
gergoerdi / CatMonad.hs
Created Jul 16, 2019
Category-indexed monads, now with more type inference!
View CatMonad.hs
-- https://stackoverflow.com/a/57046042/477476
-- https://gist.github.com/Lysxia/7331df3abee0aceacd3d9a74b567f54c
{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs, TypeOperators #-}
{-# LANGUAGE TypeApplications, RebindableSyntax #-}
import Prelude hiding (id, (.))
import Control.Category
@gergoerdi
gergoerdi / CatMonad.hs
Last active Jul 16, 2019
Category-indexed monads
View CatMonad.hs
-- https://stackoverflow.com/a/57046042/477476
-- https://gist.github.com/Lysxia/04039e4ca6f7a3740281e4e3583ae971
{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
{-# LANGUAGE GADTs, TypeOperators #-}
{-# LANGUAGE TypeApplications, RebindableSyntax, RecordWildCards #-}
import Prelude hiding (id, (.))
import Control.Category
import Data.Kind
@gergoerdi
gergoerdi / CatMonadCounter.hs
Last active Jul 16, 2019
Nat as a type-level category, to be used as the index of a category-indexed monad
View CatMonadCounter.hs
-- https://stackoverflow.com/a/57046042/477476
-- https://gist.github.com/Lysxia/04039e4ca6f7a3740281e4e3583ae971
{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
{-# LANGUAGE TypeApplications, TypeOperators, GADTs #-}
import Prelude hiding (id, (.))
import Control.Category
import Data.Kind
import GHC.TypeLits
View Int.agda
{-# OPTIONS --cubical #-}
module Int where
open import Data.Nat renaming (_+_ to _+̂_)
open import Cubical.Core.Prelude
open import Utils
Same : Set
Same x y x′ y′ = x +̂ y′ ≡ x′ +̂ y
@gergoerdi
gergoerdi / Quotient.agda
Created Nov 11, 2018
Cubical quotient types
View Quotient.agda
{-# OPTIONS --cubical #-}
module Quotient where
open import Cubical.Core.Prelude
Reflexive : {ℓ} {A : Set ℓ} (A A Set ℓ) Set _
Reflexive _∼_ = x x ∼ x
module Quot {ℓ} (A : Set ℓ) (_∼_ : A A Set ℓ) (∼-refl : Reflexive _∼_) where
data Q : Setwhere
View Printf.hs
{-# LANGUAGE GADTs, TypeInType, DataKinds, TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
import GHC.TypeLits
import GHC.Types
import Data.Singletons
import Data.Singletons.Prelude
data Format = Lit Symbol | Str | Shown Type
View NumFin.agda
open import Agda.Builtin.FromNat
open import Data.Fin
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Nat renaming (_≤?_ to _N≤?_)
open import Data.Unit
instance
NumFin : {n} Number (Fin n)
View Shub.agda
open import Data.Nat
open import Relation.Binary.PropositionalEquality renaming (subst to ≡-subst)
open import Data.Empty
open import Data.Unit
open import Relation.Binary
open import Data.Star
open import Level renaming (zero to lzero; suc to lsuc)
open import Data.Product
open import Function using (_⟨_⟩_)
-- open import Function using (_∘_; id)
You can’t perform that action at this time.