david-christiansen

module ClassNonsense

import Language.Reflection.Elab

class Foo a where
  foo : a -> () -> a

class Foo a => Bar a where
  constructor MkFoo
  bar : a -> Int

david-christiansen

module Main

import Data.So
import Debug.Trace

%include C "bytes.h"
%link C "bytes.o"

%access public

david-christiansen

mutual
  class Foo a where
    foo : a -> Type
    bar : (x : a) -> foo @{nonsense} x -> Int

  instance Foo a where
    foo x = Nat
    bar x n = 354

  instance [nonsense] Foo a where

david-christiansen

18:38:27 -> ((:docs-for "Nat")
 94)
18:38:27 <- (:return
 (:ok "Data type Nat : Type\n    Unary natural numbers\n    \nConstructors:\n    Z : Nat\n        Zero\n        \n    S : Nat -> Nat\n        Successor\n        "
      ((10 3
           ((:name "Prelude.Nat.Nat")
            (:implicit :False)
            (:decor :type)
            (:doc-overview "Unary natural numbers")
            (:type "Type")

david-christiansen

module NatInd

import Language.Reflection.Elab
import Language.Reflection.Utils

%default total

trivial : Elab ()
trivial = do compute
             g <- snd <$> getGoal

david-christiansen

||| A port of Chung-Kil Hur's Agda proof that type constructor
||| injectivity is incompatible with LEM.
|||
||| See https://lists.chalmers.se/pipermail/agda/2010/001526.html
||| and its follow-ups for a good discussion.
module AntiClassical

%default total

||| Law of the excluded middle, with an appropriately classical name

david-christiansen

module MkMonoid

import Language.Reflection.Elab

||| Generate a Monoid dictionary
total
mkMonoid : Semigroup a => (neutral : a) -> Monoid a
mkMonoid @{semigroup} neutral = mkMonoid' _ semigroup neutral
  where
    mkMonoid' : (a : Type) -> (constr : Semigroup a) -> a -> Monoid a

david-christiansen

module MkShow

import Language.Reflection.Elab

mkShow : (a : Type) -> (a -> String) -> Show a
mkShow = %runElab (fill (Var (SN (InstanceCtorN `{Show}))) *> solve)

shower : Show Float
shower = mkShow _ (const "oops")

david-christiansen

module Finite

import Data.Fin
import Language.Reflection.Elab
import Language.Reflection.Utils

%default total

||| A bijection between some type and bounded numbers
data Finite : Type -> Nat -> Type where

david-christiansen

module VeryFun

class VeryFun (f : Type -> Type) (dict : Functor f) | f where
  funIdentity : {a : Type} -> (x : f a) ->
                map @{dict} id x = id x
  funComposition : {a : Type} -> {b : Type} ->
                   (x : f a) -> (g1 : a -> b) -> (g2 : b -> c) ->
                   map @{dict} (g2 . g1) x = (map @{dict} g2 . map @{dict} g1) x

instance VeryFun List %instance where