View liftTypeRep
liftTypeRep :: TypeRep a -> TH.Type | |
liftTypeRep ty = L.foldl AppT t0 [liftTypeRep ty' | SomeTypeRep ty' <- args] | |
where | |
(con, args) = splitApps ty | |
t0 = ConT $ mkName (tyConModule con <> "." <> tyConName con) |
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], |
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 |
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 |
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 |
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 : Set ℓ where |
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) |
NewerOlder