myuon

variable {T : Type}

inductive list (T : Type) : Type :=
| nil {} : list T
| cons : T → list T → list T
open list

definition append : list T → list T → list T
| nil l := l
| (cons x xs) l := cons x (append xs l)

myuon

{-# LANGUAGE GADTs, RankNTypes, TypeOperators, DataKinds, KindSignatures #-}
{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies, ScopedTypeVariables, TypeFamilies #-}
{-# LANGUAGE FlexibleContexts, ConstraintKinds #-}
module MakeLense (
  Name(..), Proxy(..),
  UnionT,
  Union(..),
  -- keysH, keysU, HasKey,
  Has,

myuon

import Haste
import Haste.DOM
import Haste.Events
import Haste.Foreign hiding (get)
import Haste.Graphics.Canvas
import Haste.Graphics.AnimationFrame
import Control.Monad.State
import Data.IORef
import qualified Data.IntMap as IM
import Lens.Family2

myuon

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, FlexibleInstances #-}

import GHC.TypeLits

type family FuncType (as :: [*]) where
  FuncType '[] = IO ()
  FuncType (a ': as) = a -> FuncType as

data Name (s :: Symbol) = Name

myuon

theory PFAD
imports Main
begin

fun maximum where
  "maximum xs = foldr max xs 0"

lemma maximum_larger: "xs ≠ [] ⟹ (⋀x :: nat. x ∈ set xs ⟹ x ≤ maximum xs)"
proof (induct xs, simp, auto)
  fix a :: nat and xs :: "nat list" and x

myuon

{-# LANGUAGE Rank2Types, ScopedTypeVariables #-}
import Prelude hiding ((<*>), abs)
import qualified Control.Applicative as A
import Control.Monad
import Test.QuickCheck

class NearSemiring m where
  (<+>) :: m a -> m a -> m a
  zero :: m a
  (<*>) :: m a -> m a -> m a

myuon

theory Category
imports Main
begin

no_notation Fun.comp (infixl "∘" 55)

lemma equiv_refl: "equiv A R ⟹ x ∈ A ⟹ (x,x) ∈ R"
by (rule equivE, simp, rule refl_onD, simp)

lemma equiv_sym: "equiv A R ⟹ (x,y) ∈ R ⟹ (y,x) ∈ R"

myuon

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, PolyKinds, UndecidableInstances, TemplateHaskell, FlexibleContexts, AllowAmbiguousTypes #-}

import Control.Lens
import Data.Extensible
import Data.Extensible.Internal
import GHC.TypeLits

type family GetList r :: [Assoc Symbol *] where
  GetList (h :* xs) = xs

myuon

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, Rank2Types #-}
import Control.Applicative
import Control.Monad
import Data.Functor.Identity
import Data.Foldable
import Data.Monoid
import Data.Tagged

class Profunctor p where
  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d

myuon

{-# LANGUAGE TemplateHaskell #-}
module Main where
 
import Control.Lens
import Control.Monad.State
import Control.Monad.Except
import Data.Char
import Data.List
import qualified Data.IntMap as IM
import Data.List.Split (chunksOf)