MarcelineVQ

data Identity a = MkId a

(>>=) : Identity a -> (a -> Identity b) -> Identity b
(>>=) (MkId x) f = f x

pure : a -> Identity a
pure = MkId

foo : Int -> Identity Balance
foo i = do

MarcelineVQ

module Main

Semigroup b => Semigroup (a -> b) where
  f <+> g = \x => f x <+> g x

Monoid b => Monoid (a -> b) where
  neutral = const neutral

[all] Semigroup Bool where
  x <+> y  = x && y

MarcelineVQ

module Main

Semigroup b => Semigroup (a -> b) where
  f <+> g = \x => f x <+> g x

Monoid b => Monoid (a -> b) where
  neutral = const neutral

[all] Semigroup Bool where
  x <+> y  = x && y

MarcelineVQ

module Main

Semigroup b => Semigroup (a -> b) where
  f <+> g = \x => f x <+> g x

Monoid b => Monoid (a -> b) where
  neutral = const neutral

[all] Semigroup Bool where
  x <+> y  = x && y

MarcelineVQ

cabal-version: 2.2
name: ray
version: 1.0.0
build-type: Simple

common shared
  ghc-options: -Wall -rtsopts -threaded
  default-language: Haskell2010
  build-depends: base, parallel, array, deepseq, monad-par
  other-modules: Raytracing, Vec3, Scene, Image, BVH

MarcelineVQ

Feb 12 04:14:47 <MarcelineVQ>	gallais: is there a C-c C-c that expands cases into patterns if patterns [meaning the keyword] are available? What I mean is that  foo : Dec (3 ≡ 2) → ℕ; foo x = {! x  !}  will give me foo (does₁ because proof₁) = {!   !}   instead of  foo (yes proof) = {!   !}; foo (no proof) = {!   !}  and that's a bit of a hassle for a couple reasons, one of which I'm writing an issue for
Feb 12 04:16:54 <MarcelineVQ>	I expect not since that's a rabbit-hole but am asking just in case
Feb 12 04:56:27 <gallais>	MarcelineVQ: if you split further on proof₁ then Agda will resugar the yes/no patterns
Feb 12 04:58:38 <MarcelineVQ>	hmm so it will, that's interesting thank you

MarcelineVQ

{-# LANGUAGE OverloadedStrings #-}

module Lib where

import Web.Scotty
import Control.Monad.Reader

data Config = Conf Int Bool

foo :: ReaderT Config ScottyM ()

MarcelineVQ

p : ∀ {a} → bar (a ∘ Z) ≡ bar a
p {a} with a ∘ Z | q {a}
p {a} | .a | refl = refl

MarcelineVQ

We couldn’t find that file to show.

MarcelineVQ

record Category (k : Set → Set → Set) : Set₁ where
  infixr 8 _⇝_
  _⇝_ : Set → Set → Set
  _⇝_ = k
  field
    id : ∀ {x} → x ⇝ x
    _∘_ : ∀ {a b c : Set} → (b ⇝ c) → (a ⇝ b) → (a ⇝ c)
  
    unitalityˡ : ∀ {X Y} {f : X ⇝ Y} → id ∘ f ≡ f
    unitalityʳ : ∀ {X Y} {f : X ⇝ Y} → f ∘ id ≡ f