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

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

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

module Main

import Data.So
import Debug.Trace

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

%access public

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 ClassNonsense

import Language.Reflection.Elab

class Foo t where
  constructor MkFoo
  foo : t

myFoo : Foo Nat
myFoo = MkFoo 1

david-christiansen

data HList : List Type -> Type where
  Nil : HList []
  (::) : t -> HList ts -> HList (t :: ts)
%name HList xs,ys

append : HList ts -> HList ts' -> HList (ts ++ ts')
append []        ys = ys
append (x :: xs) ys = x :: append xs ys

david-christiansen

module NotElem

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

import Data.List


emptyNotElem : {a : Type} -> {x : a} -> Elem x [] -> Void
emptyNotElem Here impossible

david-christiansen

data Typ =
    IntTyp
  | BolTyp
  | FunTyp Typ Typ

toType : Typ -> Type
toType IntTyp       = Integer
toType BolTyp       = Bool
toType (FunTyp x y) = toType x -> toType y

david-christiansen

syntax mmatch [t] as {x} returning [ty] cases [cs] =
    Match (\x => ty) t cs
syntax pat {x} "." [tm] = PTele (\x  => tm)
syntax [tm1] "=>" [tm2] = PBase tm1 tm2


foo : Tac (List ())
foo = mmatch Z as y returning (List ())
      cases [