wires

Require Import 
  additional_operations.

Check (1^3).
(* 1 ^ 3
     : nat *)

Require Import Streams.

Notation "∅ x" := (Stream x) (at level 38).

wires

Section s1.
Context `{Ring R}. (* Error: Unbound and ungeneralizable variable Ring *)
(* That's a clear error message *)
End s1.

Require Import canonical_names.
Section s2.
Context `{Ring R}. (* Error: Cannot infer the type of R. *)
(* it haz confusing, why happens? *)

wires

(* http://coq.inria.fr/stdlib/Coq.Bool.Bvector.html

   Section VECTORS --> Vcons, Vextend   -- this I cannot use?
   Section BOOLEAN_VECTORS --> Bcons    -- this I can use
*)

Require Import Bvector.

Check (Bcons).

wires

Require Import Utf8 String ZArith.

(* IO is done through this JSON inductive type *)
Inductive JSON :=
  | JObject : list (string * JSON) → JSON
  | JArray : list JSON → JSON
  | JString : string → JSON
  | JNumber : Z → JSON
  | JBool : bool → JSON
  | JNull : JSON.

wires

Infix "×" := prod (at level 60).

Coercion bool_in_nat := fun b:bool => if b then 0 else 1.

Definition a : nat := false.

Definition foo (p:bool × bool) : bool × nat :=
  (fst p, snd p:nat).

Coercion fooc := foo.

wires

Require Import String.

Open Scope string_scope.
Check "tag".

Delimit Scope ex_scope with ex.

Notation "tag : body" := (tag, body) (at level 30): ex_scope.

Open Scope ex_scope.

wires

Require Import Arith.

(* Robberts check that takes a looooong time.. for breaking roosterbots :P *)
Check (tt : if let f := fix f n := match n with O => 1 | S n => f n + f n end in beq_nat (f 20) (f 20) then unit else bool).

wires

Require Import Utf8.

(*

  F⁰, F¹, F², F³, ...

  (0,1) (1,2) (2,3) (3,4)

  map ∥·∥ (F_n - F_m)

wires

Require Import canonical_names.

Class Foo A := foo: A → A.

Instance kaas0 X : Foo X := @id X.
(* kaas0 = λ X : Type, id
         : ∀ X : Type, Foo X
    
   Argument scope is [type_scope] *)

wires

Require Import
  interfaces.canonical_names
  interfaces.abstract_algebra.

(* Lazy evaluating trick. Coq is strict but a lambda term
   is not further evaluated. This allows you to trick Coq
   into lazy evaluation, like so: *)

Inductive lazy_nat : Type :=
  | lazy_O : lazy_nat