| /* Solarized Dark | |
| For use with Jekyll and Pygments | |
| http://ethanschoonover.com/solarized | |
| SOLARIZED HEX ROLE | |
| --------- -------- ------------------------------------------ | |
| base03 #002b36 background | |
| base01 #586e75 comments / secondary content |
| {-# LANGUAGE ConstraintKinds #-} | |
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE ExistentialQuantification #-} | |
| {-# LANGUAGE ExplicitNamespaces #-} | |
| {-# LANGUAGE FlexibleContexts #-} | |
| {-# LANGUAGE FlexibleInstances #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE PolyKinds #-} | |
| {-# LANGUAGE ScopedTypeVariables #-} | |
| {-# LANGUAGE TypeApplications #-} |
| // based on https://arxiv.org/pdf/1803.02294.pdf | |
| import Relation.Equality | |
| K : { X : Type} -> Type | |
| {x : X, y : X, p : Path(X,x,y), q : Path(X,x,y)} -> Path(Path(X,x,y),p,q) | |
| J : | |
| { X : Type | |
| , x : X |
| // Let's start our lawful Functor abstraction | |
| T Functor {F : Type -> Type} | |
| | functor | |
| { map : {~A : Type , ~B : Type , f : A -> B, x : F(A)} -> F(B) | |
| , identity : {~A : Type , fa : F(A)} -> map(~A, ~A, id(~A),fa) == fa | |
| , composition : | |
| { ~A : Type | |
| , ~B : Type | |
| , ~C : Type |
| import Data.Empty | |
| import Data.Unit | |
| Interval : Type | |
| $self | |
| { ~P : {i : Interval} -> Type | |
| , I0 : P(i0) | |
| , I1 : P(i1) | |
| , ~SG : I0 == I1 | |
| } -> [x : P(self) ~ I0 == I1] |
| import Relation.Binary | |
| import Relation.Equality | |
| // identity function | |
| id : {~A : Type, x:A} -> A | |
| x | |
| // composition function | |
| compose : {~A : Type, ~B : Type, ~C : Type, g : B -> C, f : A -> B, x : A} -> C | |
| g(f(x)) |
| import Data.Nat | |
| import Data.InductionTree | |
| Array : {A : Type, n : Nat} -> Type | |
| case/Nat n | |
| | succ => [x : Array(A, n.pred), Array(A, n.pred)] | |
| | zero => A | |
| : Type | |
| // :::::::::: |
| (module | |
| (type (;0;) (func (param i32))) | |
| (type (;1;) (func (result i32))) | |
| (type (;2;) (func (param i32) (result i32))) | |
| (type (;3;) (func (param f64) (result f64))) | |
| (type (;4;) (func (param f64 f64) (result f64))) | |
| (type (;5;) (func (param f64 f64) (result i64))) | |
| (type (;6;) (func (param i32 i32 i32 i32) (result i32))) | |
| (type (;7;) (func (param f64 f64) (result i32))) | |
| (type (;8;) (func (param i32 i32 i32 i32) (result f64))) |
"considering making single-line definitions with
;a syntax error to stop your kingdom of evil" --Victor Maia
The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in RFC 2119
