donovancrichton

module Category
%default total

public export
-- Heterogenous binary relations
REL : Type -> Type -> Type
REL a b = a -> b -> Type

-- Homogenous binary relations
public export

donovancrichton

module Syntax
 
%default total

namespace SR
  public export
  interface Semiring a where
    constructor MkSemiring
    ---------------------------- OPERATIONS ------------------------------------
    -- A semiring (R) has two binary operations:

donovancrichton

module PigeonHole

import Data.Nat
import Data.Vect

%default total

data Elem : a -> Vect k a -> Type where
  Here : Elem x (x :: xs)
  There : Elem x xs -> Elem x (y :: xs)

donovancrichton

module HurkensParadoxLoop

%default total

-- Caued by Type : Type

-- Negation, (x : A) -> ⊥
¬ : Type -> Type
¬ x = x -> Void

donovancrichton

module CantPatternMatchOnDPair

%default total

data Expr : Type -> Type where
  Lam : {a, b : Type} -> (a -> Expr b) -> Expr (a -> b)


-- this should be covering
f : (a : Type ** Expr a) -> (b : Type ** Expr b)

donovancrichton

module CantMatchOnSigmaFunc

%default total      
      
data Expr : Type -> Type where      
  Lam : {a, b : Type} -> (a -> Expr b) -> Expr (a -> b)         
                                                                
{-
f : (a : Type ** Expr a) -> (b : Type ** Expr b)  
f (ty ** focus) =       

donovancrichton

module CantGoLeft

%default total

data Expr : Type -> Type where
  Val : {a : Type} -> a -> Expr a
  Add : {a : Type} -> Num a => Expr a -> Expr a -> Expr a
  App : {a, b : Type} -> Expr (a -> b) -> Expr a -> Expr b
  Lam : {a, b : Type} -> (a -> Expr b) -> Expr (a -> b)

donovancrichton

------------------------------- Base Imports ---------------------------------
import Syntax.PreorderReasoning -- for long proofs
import Data.List -- for list lemmas
------------------------------ Custom Imports --------------------------------
import VerifiedFunctor

--------------------------------- Pragmas ------------------------------------
%default total
%hide Prelude.(<$>)
%hide Prelude.Interfaces.(<*>)

donovancrichton

%default total  

data Foo : Type
-- comment out the next line to have things type check.
data Bar : Foo -> Foo -> Type          
                                                                                                  
data Foo : Type where      
  MkFoo : Foo                                                                             
  
data Bar : Foo -> Foo -> Type where                                                       

donovancrichton

%default total

data Fix : (Type -> Type) -> Type where
  MkFix : f (Fix f) -> Fix f

F : Type -> Type
F x = x -> x

fix : Fix F -> Fix F
fix (MkFix f) = f (MkFix f)