mb64

umask 022

declare -x PAGER='less'
declare -x EDITOR='vim'
declare -x VISUAL="${EDITOR}"
declare -x FCEDIT="${EDITOR}"

declare -x LS_COLORS='no=01;37:fi=01;37:di=01;34:ln=01;36:pi=01;32:so=01;35:do=01;35:bd=01;33:cd=01;33:ex=01;31:mi=00;37:or=00;36:'

declare -x HISTCONTROL=ignoreboth:erasedups

mb64

f : {a : Type} -> a -> a
f {a=Int}    x = 2 * x
f {a=String} x = "twice " ++ x
f {a=_}      x = x

main : IO ()
main = do
  -- Ad-hoc polymorphism type 1: type-based overloading
  -- Also in: C++, Java
  printLn $ "hi " ++ "there" -- uses the ++ for String

mb64

/* A flat representation of
 * data Tree = Leaf Int | Node Tree Tree
 *
 * Either:
 *  - *ft is LEAF and a single int follows
 *  - *ft is NODE and two subtrees follow
 */
#define LEAF 0
#define NODE 1

mb64

.PHONY: all bench

all: bench

bench: main_c main_asm
	@echo "Running the C version..."
	@bash -c 'time ./main_c'
	@echo
	@echo "Running the asm version..."
	@bash -c 'time ./main_asm'

mb64

{-# OPTIONS --cubical --safe #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism using (Iso; isoToPath)

data N : Set where
  one : N
  _+_ : N → N → N
  assoc : (a b c : N) → (a + b) + c ≡ a + (b + c)

mb64

module Bidir

Ident : Type
Ident = String

mutual
  BaseCtx' : Type
  Ctx' : BaseCtx' -> Type
  CtxItem' : (b : BaseCtx') -> (c : Ctx' b) -> Type

mb64

module DerivingEq

import Language.Reflection

%language ElabReflection

public export
countArgs : (ty : TTImp) -> Nat
countArgs (IPi _ _ ExplicitArg _ _ retTy) = 1 + countArgs retTy
countArgs (IPi _ _ _ _ _ retTy) = countArgs retTy