• root

• blog/
• cv
• misc/

1 Test 1

test post body [1]

test :: IO ()
test = putStrLn "Test"

Require Import CoqLib.Prelude.
Notation "_ [→] _" was already used in scope
type_scope. [notation-overridden,parsing]
Notation "_ [→] _" was already used in scope
type_scope. [notation-overridden,parsing]
Notation "_ [⇒] _" was already used in scope
type_scope. [notation-overridden,parsing]

Definition bbb := Empty_set.
Search Empty_set.
Empty_set_sind: ∀ (P : ∅ → SProp) (e : ∅), P e
Empty_set_rec: ∀ (P : ∅ → Set) (e : ∅), P e
Empty_set_ind: ∀ (P : ∅ → Prop) (e : ∅), P e
Empty_set_rect: ∀ (P : ∅ → Type) (e : ∅), P e

Definition test := 0.
Check test.
test
     : nat

Lemma aaa : 1 + 1 = 2.
1 + 1 = 2
Proof.
1 + 1 = 2
  simpl.
2 = 2
  reflexivity.
Qed.

test : Bool
test = true

2 Test 2

\[\forall \, x : x\]

\[p_{ij}(t) = \frac{\ell_j(t) - \ell_i(t)}{\sum_{k \in N_i(t)}^{} \ell_k(t) - \ell_i(t)}\]

\begin{mathpar}
  \inferrule[yop]{ aa \\ bb }{ cc }
\end{mathpar}

\[ \begin{array}{c|lcr} n & \text{Left} & \text{Center} & \text{Right} \\ \hline 1 & 0.24 & 1 & 125 \\ 2 & -1 & 189 & -8 \\ 3 & -20 & 2000 & 1+10i \end{array} \]

\[ f(n) = \begin{cases} \frac{n}{2}, & \text{if $n$ is even} \\[2ex] 3n+1, & \text{if $n$ is odd} \end{cases} \]

2.1 Test 3

Bibliography