lthms

#[test]
fn test_raw() {
    assert_eq!(
        raw("Hi stranger, how are you?"),
        Ok(
            (
                "",
                Format::Raw(
                    vec![
                        Atom::Word("Hi"),

lthms

{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Main where

import           Control.Concurrent         (forkIO, threadDelay)
import           Control.Exception          (catch)
import           Control.Monad              (forever, void, when)
import           Control.Monad.State.Strict (StateT, get, runStateT)

lthms

inductive seq (α: Type) : Type
| cons : α -> seq -> seq
| nil {} : seq

open seq

def apply {α β} (f: α -> β) : seq α -> seq β
| nil := nil
| (cons x rst) := cons (f x) (apply rst)

lthms

(defvar x 3)
(defvar test (list 'x))
(eval `(setf ,(nth 0 test) 5))
(print x)

lthms

run:
        @sbcl --eval "(ql:quickload :lysk)" \
              --eval "(lysk:run)"

bundle:
        @echo -en "[ ] Remove old build"
        @rm -rf build/
        @echo -e "\r[*] Remove old build"
        @echo "[ ] Building"
        @sbcl --eval "(ql:quickload :lysk/bundle)" --eval "(lysk.bundle:deliver)" --quit

lthms

(cl:in-package :lysk)

(gamekit:defgame example () ())

(defmethod gamekit:post-initialize ((app example))
  (gamekit:bind-button :mouse-left :released
                       (lambda () (gamekit:stop))))

(defun run ()
  (gamekit:start 'example))

lthms

\usepackage[light]{noto}
\usepackage[light]{merriweather}

\makeatletter
\let\scshape\relax % to avoid a warning
\DeclareRobustCommand\scshape{%
  \not@math@alphabet\scshape\relax
  \ifnum\pdf@strcmp{\f@family}{\familydefault}=\z@
    \fontfamily{NotoSerif-TLF}%
  \fi

lthms

Require Import Coq.Arith.Mult.

Inductive tree
          (a:  Type)
  : Type :=
| Leaf (x:  a)
  : tree a
| Node (x:  a)
       (l:  tree a)
       (r:  tree a)

lthms

Require Import Coq.Program.Program.
Require Import Coq.Arith.PeanoNat.
Require Import Recdef.
Require Import Omega.

Function sup
         (n:  nat)
         {measure id}
  : nat :=
  match n with

lthms

│23:39:42    lthms | et je vais m’arrêter là pour ce soir
│23:39:49          | parce que dodo
│00:33:35          | je me suis relevé parce que j’arrivais pas à dormir à cause de ce truc