Testing Code
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>
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.