larsr

(*  Proof that you can build foldR out of foldL *)


Require Import Arith List. Import ListNotations.


Fixpoint foldR {A : Type} {B : Type} (f : A -> B -> B) (v : B) (l : list A) : B :=
  match l with
  | nil => v
  | x :: xs => f x (foldR f v xs)

larsr

Disable Device Enrollment Program (DEP) notification on macOS Catalina.md

With full reinstall (recommended)

   a. Boot into recovery using command-R during reboot, wipe the harddrive using Disk Utility, and select reinstall macOS

   b. Initial installation will run for approximately 1 hour, and reboot once

   c. It will then show a remaining time of about 10-15 minutes

larsr

#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#ifdef _MSC_VER
#include <intrin.h> /* for rdtscp and clflush */
#pragma optimize("gt",on)
#else
#include <x86intrin.h> /* for rdtscp and clflush */
#endif

larsr

# docker build -t coq .
# coqtop() (docker run --rm -v "$HOME:$HOME" -ti coq sh -c "cd $HOME ; "'coqtop $(cat ~/src/VST/_CoqProject-export)'" $@")

#FROM coqorg/coq:dev
FROM coqorg/coq:8.11.0

RUN opam init -y; \
    opam repo --set-default add coq-released https://coq.inria.fr/opam/released; \
    opam install -y -b coq-mathcomp-algebra coq-mathcomp-analysis coq-coquelicot coq-compcert
    

larsr

Creating a .so dynamic library of a haskell program and calling it from C

TLDR:

• Export a haskell function with foreign export.
• Create a C wrapper that calls hs_init when the library is loaded.
• Compile the .hs and .c wrapper with ghc, linking with lHSrts-ghc8.6.5
• Use it from C by linking as usual.

(For more details, see here.)

larsr

Haskell

import Crypto.Cipher.AES
import Data.ByteString.UTF8 (fromString, toString)
import Data.ByteString.Base16 (encode)


main = do

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)]}