lthms

import numpy.random
import numpy

class ModelNGram:
    def __init__(self, n):
        self.memory = {}
        self.nb_grams = 0
        self.lck = False
        self.n = n
        self.start = ""

lthms

// Compile error:
//   Compiling test v0.0.1 (file:///home/lethom/repos/test)
// /home/lethom/repos/test/src/main.rs:9:1: 13:2 error: the type `HelloProxy<'a>` does not fulfill the required lifetime
// /home/lethom/repos/test/src/main.rs:9 impl<'a> Hello for HelloProxy<'a> {
// /home/lethom/repos/test/src/main.rs:10     fn hello(&self) {
// /home/lethom/repos/test/src/main.rs:11         self.ptr.hello();
// /home/lethom/repos/test/src/main.rs:12     }
// /home/lethom/repos/test/src/main.rs:13 }
// note: type must outlive the static lifetime
// error: aborting due to previous error

lthms

Require Import Coq.Unicode.Utf8.

Section lists.
  Variable A:Set.

  Inductive list:Set :=
  | nil: list
  | cons: A → list → list.

  Definition empty (l:list):Prop := l = nil.

lthms

λ stack ghci
Configuring GHCi with the following packages: token
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Data.Token ( /home/lethom/repos/token/src/Data/Token.hs, interpreted )
Ok, modules loaded: Data.Token.
*Data.Token Data.Token> :set -XOverloadedStrings
*Data.Token Data.Token> :set -XDataKinds
*Data.Token Data.Token> let true = "true" :: Token "machin"
*Data.Token Data.Token> let test = "test" :: Token "test"
*Data.Token Data.Token> true == true

lthms

module Main where

import Prelude
import Control.Monad.Eff (Eff)
import Control.Monad.Eff.Console (CONSOLE, log)
import Data.Maybe (Maybe(..))
import Data.Either (Either(..))

import Control.Monad.Aff (launchAff)
import Network.HTTP.Affjax

lthms

default:
        as routine.S -o routine.o
        ld routine.o -o routine -XN

clean:
        rm -f routine.o routine

.PHONY: default clean

lthms

{-# LANGUAGE TypeFamilies #-}

module Main where

newtype WithMem a b = WithMem { unWith :: a -> (b, WithMem a b) }

instance Functor (WithMem a) where
  f `fmap` (WithMem fmem) = WithMem $ \x -> let (x', fmem') = fmem x
                                            in (f x', f `fmap` fmem')

lthms

#define _GNU_SOURCE

#include <sched.h>
#include <unistd.h>
#include <stdio.h>
#include <stdlib.h>
#include <sys/wait.h>

#define STACK_SIZE 0x20000

lthms

(* No more subgoal, yet one obligation remains *)

Program Definition software_only
        {H E: Type}
        (h: H)
        (e: E)
        {pEv: E -> Prop}
        (pEv_dec: forall (e: E), { pEv e } + { ~ pEv e })
        (pTs: H -> { e: E | pEv e } -> Prop)
  := if pEv_dec e

lthms

DEBUG:pijul::commands: get_wd: None
DEBUG:libpijul::file_operations: collecting Inode(0000000000000000),""
DEBUG:libpijul::file_operations: basename = ""
DEBUG:libpijul::file_operations: starting iterator, key=Inode(0000000000000000)
DEBUG:libpijul::backend: iter_tree: Some((FileId { parent_inode: Inode(0000000000000000), basename: "" }, None))
DEBUG:libpijul::backend: tree iter
DEBUG:libpijul::backend: tree iter: UnsafeFileId { parent_inode: Inode(0000000000000000), basename: "LICENSE" } Inode(141c73e142d55979)
DEBUG:libpijul::file_operations: iter: FileId { parent_inode: Inode(0000000000000000), basename: "LICENSE" } Inode(141c73e142d55979)
DEBUG:libpijul::file_operations: collecting Inode(141c73e142d55979),"LICENSE"
DEBUG:libpijul::file_operations: node = FileHeader { metadata: FileMetadata(420), status: Ok, key: Key { patch: PatchId 0x85d31085e7e911f0, line: LineId(0x0200000000000000) } }