Skip to content
Permalink
Browse files

✏️ Edit 'Initial commit'

  • Loading branch information...
Punie committed Apr 26, 2019
1 parent e6fafd2 commit ef31839ffbf266ccec91d5e4e2b03069c38ca6fa
Showing with 41 additions and 1 deletion.
  1. +41 −1 content/posts/00-initial-commit.md
@@ -6,9 +6,13 @@ slug: "initial-commit"

toc: false
autoCollapseToc: false

mathjax: true
mathjaxEnableSingleDollar: true
mathjaxEnableAutoNumber: true
---

# :tada: Initial Commit
# :tada:

It's been more than a year now that I wanted to try and start a blog. But being
a tad OCD means I could never settle on a title, domain name, theme or even
@@ -27,3 +31,39 @@ Oh, and by the way, I like emojis :rainbow:. They're cute. Don't be a hater!

<!--more-->

Some random additional things to take into account before you go.

I chose [gitalk](https://github.com/gitalk/gitalk) for my comment system. What
that means is that you will need a [Github](https://github.com/) account if you
plan to leave a comment (and I _really_ invite you to!). I realize that might be
inconvenient if you are not a tech person but I truly hate
[disqus](https://disqus.com/) with a passion.

I won't talk _only_ about software engineering or computer science subjects. I
happen to be french, so naturally I **love** food and I **love** cooking and I
am really, _really_ passionate about it so there is a good chance I will write
about it from time to time.

Finally, I promised you some niche language snippets and weird math formulas so
here you go:

- a little bit of [idris](https://www.idris-lang.org/) wisdom (unfortunately,
[chroma](https://github.com/alecthomas/chroma/) highlighting is quite buggy
with idris still)

```idris
zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith _ [] [] = []
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
```

- the rules of induction for the natural numbers
- $Rule 1$ : $0$ is a natural number
- $Rule 2$ : if $n$ is a natural number, then $succ(n)$ is a natural number

$$
\begin{array}{cl}
\displaystyle\frac{}{0 : \mathtt{Nat}} & {(Rule 1)} \\\\ \\\\ \\\\ \\\\
\displaystyle\frac{n : \mathtt{Nat}}{\mathtt{succ}(n) : \mathtt{Nat}} & {(Rule 2)} \\\\ \\\\ \\\\ \\\\
\end{array}
$$

0 comments on commit ef31839

Please sign in to comment.
You can’t perform that action at this time.