tel

runghc Main.hs preview
LInitialising
  [   0ms] Creating store
istening on http://0.0.0.0:8000/
  [   5ms] Creating provider
Adding new compilers
Compiling css/bootstrap.css
  [ 646ms] Total compile time
  [   1ms] Routing to css/bootstrap.css
Compiling css/bootstrap.min.css

tel

Command: (default View) 

tel

acm

tel

open import Data.Vec

tel

 as F using (Fin; zero; suc)
open import Data.List as L using (List; []; _∷_)
open import Data.Vec as V using (Vec; []; _∷_)

open import Category.Monad
open import Category.Monad.Indexed

private
 module Monadic {m} {M : Set m → Set m} (Mon : RawMonad M) where

tel

n + n ≡ m + m

tel

module Logic where

data _∧_ (P Q : Set) : Set where
  conj : P → Q → P ∧ Q

data _∨_ (P Q : Set) : Set where
  injl : P → P ∨ Q
  injr : Q → P ∨ Q

tel

 #-}

module Hurkens where

⊥ : Set
⊥ = (A : Set) -> A

¬_ : Set -> Set
¬ A = A -> ⊥

tel

Exercise: 4 stars, optional (filter_challenge)

filter : ∀ {A : Set} → (A → Bool) → List A → List A

tel

thm l1 l2 l p merge all-l1 all-l2 = {!