larsr

cat >demo.hs <<EOF
quicksort [] = []
quicksort (p:xs) = (quicksort lesser) ++ [p] ++ (quicksort greater)
  where
    lesser  = filter (<  p) xs
    greater = filter (>= p) xs

main = print(quicksort([5,2,1,0,8,3]))
EOF

larsr

(* Proof that 0.9999999999... = 1 *)

Require Import Reals.
From Coquelicot Require Import Coquelicot.
Require Import Psatz.

Definition nine i := (9/10)*(1/10)^i.

Example e1: sum_n nine 3 = 9/10 + 9/100 + 9/1000 + 9/10000.
  unfold nine.

larsr

(**
  
Which answer is correct?
 1. All of the below.
 2. None of the below.
 3. All of the above.
 4. At least one of the above.
 5. None of the above.
 6. None of the above.

larsr

import Data.Char
import Data.Functor
import Data.List
------------------------------------------------------------
import Control.Monad
import Control.Applicative
import Data.List

newtype Parser a = Parser { parse :: String -> [(a, String)]} 

larsr

""" Announcing and locating a service """

import socket
import atexit
import multiprocessing
import time
import pickle
import zeroconf

larsr

Require Import Arith.
Require Import Program.

Program Fixpoint sumn (n:nat) {measure n} :=
  if dec (n =? 0) then 0 else n + sumn (n-1).
Next Obligation.
  destruct n; simpl in H.
  congruence.
  auto with arith.
Defined.

larsr

# Lars.Rasmusson@gmail.com, 2019-01-12

from numpy import *

def gcd(n, m):
    n, m = min(n, m), max(n, m)
    while n != 0: n, m = m % n, n
    return m

def experiment(N):

larsr

(* 
   Coq proof of Hofstadter's MU puzzle (https://en.wikipedia.org/wiki/MU_puzzle) 
    
   To prove that "MU" cannot be generated, 
   show by induction on a valid string that the number of "I"
   is never a multiple of three.
   Then as a corollary we see that "MU" which has zero "I" cannot be
   a valid string. 

   Lars.Rasmusson@gmail.com, 2018-12-17

larsr

From Coquelicot Require Import Coquelicot.
Import Even.
Require Import Reals.
Require Import Psatz.
Import Complex.


Notation "x !" := (fact x) (at level 30). (* tighter than mul and div *)

Lemma is_series_cos x: is_series (fun i : nat => (-1) ^ i / INR ((2 * i) !) * x ^ (2*i)) (cos x).

larsr

(* Definition of exponential for complex numbers 
  Lars.Rasmusson@gmail.com, 2018-10-06
  *)

From Coquelicot Require Import Coquelicot.
Require Import Reals.
Require Import Psatz.
Import Complex.