david-christiansen

module FizzBuzzC

%default total

-- Dependently typed FizzBuzz, constructively

-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
  ZeroFizzy : Fizzy 0
  Fizz : Fizzy n -> Fizzy (3 + n)

david-christiansen

||| Binary parsing, based on the stuff in Power of Pi
module Bin


import System

import Data.So
import Data.Vect
import Bytes

david-christiansen

module Main

import Data.Vect
import Data.Fin

%default total

||| If a value is neither at the head of a Vect nor in the tail of
||| that Vect, then it is not in the Vect.
notHeadNotTail : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))

david-christiansen

package dep

import scala.language._

object Dep extends App {

  sealed trait Nat {
    type Plus[M <: Nat] <: Nat
    def plus[M <: Nat](m: M): Plus[M]
  }

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

Keybase proof

I hereby claim:

• I am david-christiansen on github.
• I am d_christiansen (https://keybase.io/d_christiansen) on keybase.
• I have a public key whose fingerprint is 2709 89EB 2214 50FA DD57 54A8 34B5 BFDB 0942 94C3

To claim this, I am signing this object:

david-christiansen

import Language.Reflection.Elab

namespace Tactics

  ||| Restrict a polymorphic type to () for contexts where it doesn't
  ||| matter. This is nice for sticking `debug` in a context where
  ||| Idris can't solve the type.
  simple : {m : Type -> Type} -> m () -> m ()
  simple x = x

david-christiansen

module JSON

import Data.HVect

import Control.Monad.Identity

import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings

david-christiansen

module NatInd

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

%default total

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

david-christiansen

module PreOrderReasoning


-- QED is first to get the precedence to work out. It's just refl with an explicit argument.
syntax [expr] "QED" = qed expr
-- foo ={ prf }= bar ={ prf' }= fnord QED
-- is a proof that foo is related to fnord, with the intermediate step being bar, justified by prf and prf'
syntax [from] "={" [prf] "}=" [to] = step from prf to

--These are the components for using the syntax with equality