xuanruiqi

%default total

data Tree : (a : Type) -> Nat -> Type where
     Leaf : Ord a => Tree a 0
     Node2 : {h : Nat} -> Tree a h -> a -> Tree a h -> Tree a (S h)
     Node3 : {h : Nat} -> Tree a h -> a -> Tree a h -> a -> 
                         Tree a h -> Tree a (S h)
                               
height : Tree a n -> Nat
height Leaf = 0

xuanruiqi

import public Data.ZZ

record IsGroup (x : Type) ((*) : x -> x -> x) (e : x) where
  constructor PrfGrp
  associative : (a : x) -> (b : x) -> (c : x) -> a * (b * c) = (a * b) * c
  identity : (a : x) -> (a * e = a, e * a = a)
  inverse : (a : x) -> (a' : x ** (a * a' = e, a' * a = e))

intIsGroup : IsGroup ZZ (+) (Pos Z)
intIsGroup = let assocInt = plusAssociativeZ

xuanruiqi

Keybase proof

I hereby claim:

• I am xuanruiqi on github.
• I am xuanruiqi (https://keybase.io/xuanruiqi) on keybase.
• I have a public key ASASNiLPeBiEeRekpmssXtGYzMo4ubz1J1MqtSYgTOFQVAo

To claim this, I am signing this object:

xuanruiqi

(define (fact-cps* n k)
  (if (= n 0)
      (k 1) ;; "throw" 1 into the continuation and we're done
      ;; CPS is a bit like accumulator style
      (fact-cps* (- n 1) ;; recurse with (- n 1)
                 (lambda (v) (k (* n v)))))) ;; throw result into continuation

xuanruiqi

data Ty = N
        | Arrow Ty Ty

-- Lexer: token definition
public export
data Token = Var String
           | Keyword String
           | Symbol String
           | Ignore String