kik

   2288 n
   1741 x
   1506 apply
   1273 m
   1272 auto
   1116 rewrite
   1016 destruct
    961 in
    947 a
    881 intros

kik

Require Import ZArith.
Require Import Zminmax.
Require Import List.
Open Scope Z_scope.

Inductive Robo : Set := Blue | Orange.
Inductive Order : Set := order : Robo -> Z -> Order.

Inductive Move : Set := Left | Right | Push | Stay.
Inductive Moves : Set := moves : Move -> Move -> Moves.

kik

Require Import ZArith.
Require Import List.
Open Scope Z_scope.

Inductive Robo : Set := Blue | Orange.
Inductive Order : Set := order : Robo -> Z -> Order.

Inductive Move : Set := Left | Right | Stay.
Inductive Moves : Set :=
| moves : Move -> Move -> Moves

kik

Require Import ZArith Znumtheory.

Open Scope Z_scope.

Section ZP.

  Record ZP := zp { quot : Z; denom : positive }.

  Definition ZP_eq (x y : ZP) :=
    quot x * (Zpos (denom y)) = quot y * (Zpos (denom x)).

kik

Require Import ZArith.
Require Import List.
Open Scope Z_scope.

Set Implicit Arguments.
Unset Strict Implicit.

Inductive Robo : Set := Blue | Orange.
Inductive Order : Set := order : Robo -> Z -> Order.

kik

Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
Require Import choice fintype tuple finfun ssralg.
Require Import ssrz smallord.
Require Import ZArith.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Inductive Robo : Set := Blue | Orange.

kik

Definition foo (x : bool) (e : x = true) := tt.

Definition bar (x : bool) : unit :=
match x as y return x = y -> unit with
| true => fun e => foo x e
| false => fun _ => tt
end (eq_refl x).

kik

Class fmonad (M : (Type -> Type) -> Type) := {
  fmreturn : forall {A : Type -> Type} {B}, (B -> A B) -> M A;
  fmbind : forall {A B : Type -> Type} {C}, M A -> ((C -> A C) -> M B) -> M B
}.

Class ST (T : (Type -> Type) -> Type) := {
  monadOfST :> fmonad T;
  runST : forall {A}, T (fun _ => A) -> A
}.

kik

(*
 * http://mattam.org/repos/coq/prelude/ を改造
 * Matthieu さんおれおれCoq使ってるから通らないところを頑張りつつ、SetoidをSetoidClassで定義してるのに置き換えてみた
 *)

Require Import Program FunctionalExtensionality Morphisms Classes.Equivalence Setoid.

Open Scope equiv_scope.
Open Scope program_scope.
Local Open Scope signature_scope.

kik

kik@icfpc-debian:~/tmp$ file /usr/share/ocamlmakefile/OCamlMakefile 
/usr/share/ocamlmakefile/OCamlMakefile: ASCII English text
kik@icfpc-debian:~/tmp$ cat Makefile 
include /usr/share/ocamlmakefile/OCamlMakefile
kik@icfpc-debian:~/tmp$ make
make[1]: Entering directory `/home/kik/tmp'
make[1]: OCamlMakefile: No such file or directory
make[1]: *** No rule to make target `OCamlMakefile'.  Stop.
make[1]: Leaving directory `/home/kik/tmp'
make: *** [byte-code] Error 2