nkaretnikov

    interiorFoldLemma :
      (pq : [ P -:> Q ])(qalg : Algebra (CUTTING C) Q)
      (f : [ Interior C P -:> Q ]) ->
      ((i : I)(p : P i) -> pq i p == f i (tile p)) ->
      ((i : I)(c : Cuts i)(ps : All (Interior C P) (inners c)) ->
        qalg i (c 8>< all f (inners c) ps) == f i < c 8>< ps >) ->
      (i : I)(pi : Interior C P i) -> interiorFold pq qalg i pi == f i pi

    interiorFoldLemma pq qalg f base step i (tile x) = base i x
    interiorFoldLemma pq qalg f base step i < c 8>< pi >

nkaretnikov

-- XXX: Combine these using a type family?
-- (You can remove the RHSs if you don't need them.)
data Brunette = Brunette
data Blonde = Blonde
data Redhead = Redhead

data Hair a = Hair a
data Height = Short | Tall

type List a = [a]

nkaretnikov

vTabulate : {n : Nat}{X : Set} -> (1 <= n -> X) -> Vec X n
vTabulate {zero} f = []
-- _>>_ : {X Y Z : Set} -> (X -> Y) -> (Y -> Z) -> (X -> Z)
-- f : 1 <= suc n -> X
-- f >> g : 1 <= suc n -> Z
-- Q: What would be a useful Z in this case?
-- A: Vec X n
-- So:
-- f >> g : 1 <= suc n -> Vec X n
-- g : X -> Vec X n

nkaretnikov

_o>>_ : {p n m : Nat} -> p <= n -> n <= m -> p <= m
oz o>> n<=m = n<=m
os p<=n o>> os n<=m = os (p<=n o>> n<=m)
os p<=n o>> o' n<=m = os ((o' p<=n) o>> n<=m)
o' p<=n o>> os n<=m = o' (p<=n o>> n<=m)
o' p<=n o>> o' n<=m = o' ((o' p<=n) o>> n<=m)

{-
oz o>> th' = th'
os oz o>> th' = th'

nkaretnikov

(add-to-list 'load-path "~/.emacs.d/evil")
(require 'evil)
(evil-mode 1)

;; Highlight matching parens.
(show-paren-mode 1)

;;; No tabs.
(setq-default ident-tabs-mode nil)
(setq-default tab-width 4)

nkaretnikov

open import Level
module Category {o ℓ e : Level}  where

open import Relation.Binary using (Rel; IsEquivalence; module IsEquivalence; Reflexive; Symmetric; Transitive) renaming (_⇒_ to _⊆_)


-- Definition of a category.
-- From https://github.com/copumpkin/categories/blob/master/Categories/Category.agda
record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where

nkaretnikov

$ apt-cache search linux-image
linux-headers-3.16.0-4-amd64 - Header files for Linux 3.16.0-4-amd64
linux-image-3.16.0-4-amd64 - Linux 3.16 for 64-bit PCs
linux-image-3.16.0-4-amd64-dbg - Debugging symbols for Linux 3.16.0-4-amd64
linux-image-amd64 - Linux for 64-bit PCs (meta-package)
linux-image-amd64-dbg - Debugging symbols for Linux amd64 configuration (meta-package)
linux-headers-4.9.0-0.bpo.4-amd64 - Header files for Linux 4.9.0-0.bpo.4-amd64
linux-headers-4.9.0-0.bpo.4-rt-amd64 - Header files for Linux 4.9.0-0.bpo.4-rt-amd64
linux-headers-4.9.0-0.bpo.5-amd64 - Header files for Linux 4.9.0-0.bpo.5-amd64
linux-headers-4.9.0-0.bpo.5-rt-amd64 - Header files for Linux 4.9.0-0.bpo.5-rt-amd64

nkaretnikov

#include <iostream>

using namespace std;

template<int N>
void f(void)
{
  cout << N << endl;
}

nkaretnikov

#include <iostream>
#include <string>
#include <vector>

using namespace std;

// lst1 = ( (a b) c &lst2 )
// lst2 = ( &lst1 )

enum class Type : bool {

nkaretnikov

#include <iostream>
#include <sstream>
#include <string>
#include <regex>

using namespace std;

int main()
{
    ostringstream oss;