Taneb

-- built on top of https://github.com/Taneb/agda-stdlib/commit/019b683a226a9eda942186aeab4b8d6be325e69c

{-# OPTIONS --without-K --safe #-}

module Lagrange where

open import Algebra.Bundles
open import Algebra.Core
open import Algebra.Morphism.Structures
open import Algebra.Properties.Group

Taneb

{-# OPTIONS --safe --without-K #-}

module Categories.Comonad.Distributive where

open import Categories.Category
open import Categories.Category.Construction.F-Algebras
open import Categories.Comonad
open import Categories.Functor
open import Categories.Functor.Algebra
open import Categories.Functor.DistributiveLaw

Taneb

{-# OPTIONS --safe --without-K #-}

module Categories.Functor.Example.Vec where

open import Categories.Category.Core using (Category)
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
open import Categories.Category.Instance.Nat
open import Categories.Category.Instance.Sets
open import Categories.Category.Monoidal.Construction.Product using (Product-Monoidal)

Taneb

// the golden ratio
phi = (sqrt(5) + 1) / 2;

// the points of a regular dodecahedron, oriented "somehow" 
dodecahedron_points = 
  [ [  1 ,  1 ,  1 ] // 0
  , [  1 ,  1 , -1 ]
  , [  1 , -1 ,  1 ]
  , [  1 , -1 , -1 ]
  , [ -1 ,  1 ,  1 ] // 4

Taneb

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module LogicT where

import Control.Applicative
import Control.Monad
import Data.Monoid

Taneb

class ReadOnly api where
  readOnly :: Proxy api -> ServerT api Handler -> ServerT api Handler

instance (ReadOnly a, ReadOnly b) => ReadOnly (a :<|> b) where
  readOnly (Proxy :: Proxy (a :<|> b)) (a :<|> b) = (readOnly (Proxy :: Proxy a) a :<|> readOnly (Proxy :: Proxy b) b)

instance (ReadOnly api) => ReadOnly (Description desc :> api) where
  readOnly (Proxy :: Proxy (Description desc :> api)) api = readOnly (Proxy :: Proxy api) api

instance (ReadOnly api) => ReadOnly ((path :: Symbol) :> api) where

Taneb

module Regex where

import Control.Applicative
import Data.Profunctor

data Regex c a = Regex (Maybe a) (c -> Regex c a)

instance Functor (Regex c) where
  fmap f (Regex xm xr) = Regex (fmap f xm) (fmap f . xr)

Taneb

module Yes where

open import Codata.Musical.Notation

open import Data.List using (List; []; _∷_)
open import Data.String using (String; unwords; _++_)
open import Data.Unit using (⊤)

open import Function using (case_of_)

Taneb

{-# LANGUAGE DataKinds #-}
module GenerateStatus where

import qualified Network.HTTP.Types.Status as Status
import GHC.TypeNats

class KnownNat n => KnownStatus n where
  statusVal :: proxy n -> Status.Status

instance KnownStatus 100 where

Taneb

pkgself: pkgsuper:

{
  haskell = pkgsuper.haskell // {
    packageOverrides = self: super: {
      Agda = pkgself.haskell.lib.doJailbreak super.Agda;
      time-compat = pkgself.haskell.lib.doJailbreak super.time-compat;
    };
  };
}