J0J0

#!/usr/bin/env ruby
#encoding: utf-8
#v0.2

if RUBY_VERSION.start_with?("1.8")
  $KCODE = "u"
  require 'rubygems'
end

require 'taglib'

J0J0

#!/usr/bin/env ruby
# encoding: utf-8

require 'nokogiri'
require 'open-uri'
begin
  require('htmlentities')
  Coder = HTMLEntities
rescue LoadError
  # dummy coder

J0J0

#!/usr/bin/env ruby
# encoding: utf-8

require 'nokogiri'
require 'open-uri'
begin
  require('htmlentities')
  Coder = HTMLEntities
rescue LoadError
  # dummy coder

J0J0

Require Import List.

(* 
   currently I'm only using these letters for sake of simplicity 
   - will expand to full alphabet later 
       (although the amount of available letters ought to be arbitrary)
*)
Inductive letter : Type :=
  a | e | o | u : letter.

J0J0

#!/usr/bin/env ruby
# encoding: utf-8

f = ARGV[0] || exit(1)

# get page count
n = `pdfinfo #{f} | grep Pages | cut -d":" -f2`.strip.to_i

# create empty page
`cd /tmp && convert -page A4 xc:white __blankpage.pdf`

J0J0

import System.Environment (getArgs)

data Dir = U | R deriving(Show)
type Link = [Dir]

shuf :: Link -> Int -> Int -> [Link]
shuf ds 0 0 = [ds]
shuf ds 0 q = shuf (R:ds) 0 (q-1)
shuf ds p 0 = shuf (U:ds) (p-1) 0
shuf ds p q =

J0J0

#!/usr/bin/env ruby

require 'yaml'

f = ARGV.shift || exit(1)
y = YAML.load_file(f)

def make_cmd(article_file, article_name, editor_name)
  
  fields = [ "#{article_file}.tex".ljust(33),

J0J0

fibs :: (Integral a) => [a]
fibs = 1 : 1 : zipWith (+) fibs (tail fibs)

--https://projecteuler.net/problem=2
problem2 :: (Integral a, Integral b) => a -> b
problem2 n
  | n <= 1 = 0
  | otherwise = sum (filter even (takeWhile (<= (fromIntegral n)) fibs))
 
answer = problem2 (4*10^6)

J0J0

Require Import List.
Import ListNotations.
Definition head := hd_error.
Definition tail := tl.
Definition len  := length.

(* make the type parameter "invisible" to the user,
   e.g. the type of 'len' is
      list ?1 -> nat

J0J0

(****************************************)
(* datatypes and functional programming *)
(****************************************)

(* We can define (inductive) datatypes like in Haskell
   (where 'Set' corresponds to Haskell's '*')
*)
Inductive mynat : Set
  := zero : mynat | plus1 : mynat -> mynat.