Testing Code

3 minute read

Consider a language, \(\mathscr{L}_0^{\N_0} \ell\),

\[\begin{equation} \begin{split} a &=b+c\\ &=e+f \end{split} \end{equation}\] \[\begin{CD} A @>a>> B \\ @VbVV @AAcA \\ C @= D \end{CD}\] \[x = \begin{cases} a &\text{if } b \\ c &\text{if } d \end{cases}\] \[\begin{rcases} a &\text{if } b \\ c &\text{if } d \end{rcases}⇒…\] \[\sum_{ \begin{subarray}{l} i\in\Lambda\\ 0<j<n \end{subarray}}\] \[N_0\] \[f(x) = \int_{-\infty}^\infty \hat f(\xi)\,e^{2 \pi i \xi x} \,d\xi\] \[c = \pm\sqrt{a^2 + b^2}\] \[\f\hat\xi\,e^{2 \pi i \xi x}\] \[\f\relax{x} = \int_{-\infty}^\infty \f\hat\xi\,e^{2 \pi i \xi x} \,d\xi\]

Let’s talk about haskell. Here is some sample code.

<!DOCTYPE HTML>

Nat
module Nat where

open import Data.Nat using ( ; _+_ ; zero; suc)

data Nat : Set where
  z : Nat
  s : Nat  Nat

Nat2ℕ : Nat  
Nat2ℕ z = zero
Nat2ℕ (s n) = suc (Nat2ℕ n)
module Nat where

open import Data.Nat using ( ; _+_ ; zero; suc)

data Nat : Set where
  z : Nat
  s : Nat  Nat

Nat2 : Nat  
Nat2 z = zero
Nat2 (s n) = suc (Nat2 n)

+-identity :  (n : )  n + zero  n
+-identity zero = refl
+-identity (suc n) rewrite +-identity n = refl

+-suc :  (m n : )  m + suc n  suc (m + n)
+-suc zero n = refl
+-suc (suc m) n rewrite +-suc m n = refl

+-comm :  (m n : )  m + n  n + m
+-comm m zero rewrite +-identity m = refl
+-comm m (suc n) rewrite +-suc m n | +-comm m n = refl

a :: [Int]
a = [1..100]

b :: [Int]
b = [2..200]

c = a ++ b

By contrast, here is some ruby code.

Here’s some attempted kramdown : \(\frac{A \quad b}{c}\)

\[\frac{\Gamma \vdash \quad b}{c}\] \[\frac{\Gamma \vdash A\hspace{2em} \Gamma, x {:} A \vdash B} {\Gamma \vdash \Pi x {:} A. B}\] \[\frac{\Gamma \vdash A = A'\hspace{2em} \Gamma, x {:} A \vdash B=B'} {\Gamma \vdash \Pi x {:} A. B = \Pi x {:} A'. B'}.\] \[\frac {\Gamma \vdash f {:} \Pi x {:} A.B\hspace{2em}\Gamma \vdash a {:} A} {\Gamma \vdash f\,a {:} B[x := a]}\] \[\frac{\Gamma \vdash A {:} U\hspace{2em} \Gamma, x {:} A \vdash B {:} U} {\Gamma \vdash \Sigma x {:} A.\, B {:} U} \hspace{3em} \frac{\Gamma \vdash A {:} U\hspace{2em} \Gamma, x {:} A \vdash B {:} U} {\Gamma \vdash \Pi x {:} A.\, B {:} U}\]

elim rule for nat \(\frac{ \Gamma, x {:} \N \vdash C \hspace{1em} \Gamma \vdash c {:} \N \hspace{1em} \Gamma \vdash d {:} C[x := 0] \hspace{1em} \Gamma, y {:} \N, z {:} C[x := y] \vdash e {:} C[x := s(y)] } { \Gamma \vdash \R(c,d,yz.e) {:} C[x := c] }\)

\[\begin{array}{rcl} U & \xrightarrow{\eta\,\circ\,U} & UFU \\ & \searrow & \downarrow \scriptsize{U \circ \eta} \\ & & U \end{array} \hspace{3em} \begin{array}{rcl} F & \xrightarrow{F\,\circ\,\eta} & FUF \\ & \searrow & \downarrow \scriptsize{\xi \circ F} \\ & & F \end{array}\] \[\frac{\Gamma \vdash A {:} U\hspace{2em} \Gamma, x {:} A \vdash B {:} \U}{c}\]

\(\frac{\Gamma \vdash b \quad \Gamma \vdash b'}{c}{d}\) \(\frac{\Gamma \vdash b \quad \Gamma \vdash b'}{\frac{c}{d}}\)

\[\frac{\Gamma \vdash A {:} U\hspace{2em} \Gamma, x {:} A \vdash B {:} \U}{\Gamma \vdash \Sigma x {:} A.\, B {:} \U} \hspace{3em}\] \[\frac{\Gamma \vdash A {:} \U\hspace{2em} \Gamma, x {:} A \vdash B {:} \U}{\Gamma \vdash \Pi x {:} A.\, B {:} \U}\]

Here’s some attempted kramdown : \(2 + 2\).

def print_hi(name)
  puts "Hi, #{name}"
end
print_hi('Tom')
#=> prints 'Hi, Tom' to STDOUT.

Check out the Jekyll docs for more info on how to get the most out of Jekyll. File all bugs/feature requests at Jekyll’s GitHub repo. If you have questions, you can ask them on Jekyll Talk.