JT Paasch jtpaasch

OCaml Systems Programming

Including the `unix` module

To compile

Compile your modules first, e.g.:

OCaml Projects

Simple project

Create a folder called myutility, with a Makefile, as well as a src subfolder:

mkdir ~/myutility

Coq Dockerfiles

These are just experiments. Turns out the ocaml/opam docker containers only use a local copy of the opam repo, so opam update does nothing. Consequently, opam install coq.8.8.1 (for instance) would always say No such package. After I learned that I simply needed to add a remote opam repository to the docker container, regular opam install X started to work again, so my docker files got simpler.

I'm putting these here just to save them somewhere. There are little

Sequence (from Jane Street Core)

Suppose you have a list.

let x = ["a"; "b"; "c"];;

Convert it to a sequence:

	(* CLI =============================== *)

	let pid_value = ref (-1)
	let get_pid () = !pid_value

	let check () =
	match get_pid () with
	\| (-1) ->
	Printf.printf "Error. Please provide a PID.\n%!";
	exit 1

	(** * Basics: Functional Programming in Coq *)

	(* REMINDER:

	#####################################################
	### PLEASE DO NOT DISTRIBUTE SOLUTIONS PUBLICLY ###
	#####################################################

	(See the [Preface] for why.)
	*)

	(** * Lists: Working with Structured Data *)

	Require Export Induction.
	Module NatList.

	(* ################################################################# *)
	(** * Pairs of Numbers *)

	(** In an [Inductive] type definition, each constructor can take
	any number of arguments -- none (as with [true] and [O]), one (as

	(** * Induction: Proof by Induction *)

	(** Before getting started, we need to import all of our
	definitions from the previous chapter: *)

	Require Export Basics.

	(** For the [Require Export] to work, you first need to use
	[coqc] to compile [Basics.v] into [Basics.vo]. This is like
	making a [.class] file from a [.java] file, or a [.o] file from a

	(** * Poly: Polymorphism and Higher-Order Functions *)

	(* Final reminder: Please do not put solutions to the exercises in
	publicly accessible places. Thank you!! *)

	(* Suppress some annoying warnings from Coq: *)
	Set Warnings "-notation-overridden,-parsing".
	Require Export Lists.

	(* ################################################################# *)

	(** * Tactics: More Basic Tactics *)

	(** This chapter introduces several additional proof strategies
	and tactics that allow us to begin proving more interesting
	properties of functional programs. We will see:

	- how to use auxiliary lemmas in both "forward-style" and
	"backward-style" proofs;
	- how to reason about data constructors (in particular, how to use
	the fact that they are injective and disjoint);