This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/* 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
.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' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Bidir | |
Ident : Type | |
Ident = String | |
mutual | |
BaseCtx' : Type | |
Ctx' : BaseCtx' -> Type | |
CtxItem' : (b : BaseCtx') -> (c : Ctx' b) -> Type |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
NewerOlder