donovancrichton

Theorem plus_id_example : ∀ n m:nat,
  n = m →
  n + n = m + m.
Proof.
  (* move both quantifiers into the context: *)
  intros n m.
  (* move the hypothesis into the context: *)
  intros H.
  (* rewrite the goal using the hypothesis: *)
  rewrite → H.

donovancrichton

%default total 

-- Our type of rose trees.
data PfTree : Type -> Type where
  Grow : a -> List (PfTree a) -> PfTree a

-- We want to show that recursion on rose trees is well-founded.
-- This is a little tricky. Idris has pre-existing well-founded proofs in the
-- prelude (WellFounded.idr). These are designed in such a way that if one can
-- conform to a 'Sized' interface, then the proof of well founded recursion is

donovancrichton

%default total

data Expr : Type -> Type where
  Var : a -> Expr a
  App : Expr a -> Expr b -> Expr a

GoLeft : Expr a -> Maybe Type 
GoLeft (Var x) = Nothing
GoLeft (App {a} x y) = Just a

donovancrichton

%default total

||| A stream (an infinite list) of natural numbers representing the
||| fibbonacci sequence.
fibs : Stream Nat 
fibs = f 0 1 
  where
    f : Nat -> Nat -> Stream Nat 
    f a b = a :: f b (a + b)

donovancrichton

%default total

interface Queue (q: Type -> Type) where   
  empty : q a 
  isEmpty : q a -> Bool
  snoc : q a -> a -> q a 
  head : q a -> a
  tail : q a -> q a 

data CatList : (Type -> Type) -> Type -> Type where

donovancrichton

%default total

interface Queue (q: Type -> Type) where   
  empty : q a 
  isEmpty : q a -> Bool
  snoc : q a -> a -> q a 
  head : q a -> a
  tail : q a -> q a 

data CatList : (Type -> Type) -> Type -> Type where

donovancrichton

--module Queue
 
import Syntax.WithProof
 
%default total
   
data State = Empty | NonEmpty
 
Eq State where
  Empty == Empty = True

donovancrichton

data ParamType = OptionParams
               | FlagParams
               | ArgParams
               | CmdParams

data Visibility = Visible
                | Hidden
                | Internal

donovancrichton

%default total 
data Term : Type -> Type where
  Const : {a : Type} -> a -> Term a
  Pair : {a : Type} -> {b : Type} -> Term a -> Term b -> Term (a, b)
  App : {a : Type} -> {b : Type} -> Term (a -> b) -> Term a -> Term b

GoLeft : {a : Type} -> Term a -> Maybe Type
GoLeft (Const x) = Nothing
GoLeft (Pair {a} x y) = Just a
GoLeft (App {a} {b} f x) = Just (a -> b)

donovancrichton

data MyList : Type -> Type where
  Nil : {a : Type} -> MyList a
  (::) : {a : Type} -> a -> MyList a -> MyList a

f : MyList a -> ()
f [] = ()
f (x :: xs) = ?normal

g : MyList a -> ()
g [] = ()