mathink

Require Import Wellfounded.
Require Import List.

(** * Structural Recursive foldr & Well-founded Recursive foldr  *)
Section FoldR.

  Context {A B: Set}(op: A -> B -> B)(e: B).

  (** ** normal foldr *)
  Fixpoint foldr (l: list A) :=

mathink

Require Import Wellfounded.
Require Import List.

(** * Structural Recursive fold & Well-founded Recursive fold 
    ** foldr
 *)

Section FoldR.

  Context {A B: Set}(op: A -> B -> B)(e: B).

mathink

Require Import Wellfounded.
Require Import List.

(** * Structural Recursive fold & Well-founded Recursive fold 
    ** foldr
 *)

Section FoldR.

  Context {A B: Set}(op: A -> B -> B)(e: B).

mathink

Inductive leq (n: nat): nat -> Set :=
| leq_n : leq n n
| leq_S (m: nat): n <= m -> leq n m -> leq n (S m).

Lemma leq_n_unique:
  forall (n: nat)(H: leq n n),
    H = leq_n n.
Proof.
  intros n H.
  destruct H.                   (* fail... *)

mathink

Module Type Ma.
Parameter R : Type.
End Ma.
 
Module Type Mb (A : Ma).
Include A.
Definition tmp := R.
Back.
Back.
Back.

mathink

(* モナドを作ってみましょう *)

Set Implicit Arguments.
Unset Strict Implicit.

Notation 型全体 := Type.
Notation 命題 := Prop.

Notation "T '上の変換'" := (T -> T) (at level 55, left associativity).
Notation "X 'から' Y 'への関数'" := (X -> Y) (at level 60, right associativity).

mathink

Set Implicit Arguments.
Unset Strict Implicit.
Generalizable All Variables.

Local Close Scope type_scope.

Definition id {A}: A -> A := fun x => x.
Definition id_ (A: Type) := id (A:=A).
Hint Unfold id id_.

mathink

Require Import ssreflect eqtype ssrbool ssrfun ssrnat seq.
Require Import Adlibssr.btree Adlibssr.binsearch Adlibssr.order.



(* leq is total-order on nat *)
Program Canonical Structure leq: totalOrder nat := makeTotalOrder leq.
Next Obligation.
  apply anti_leq.
Qed.

mathink

(* -*- mode: coq -*- *)
(* Time-stamp: <2014/9/6 1:2:55> *)
(*
  Scratch.v 
  - mathink : Author
 *)

(** * Category Theory 'on' Coq *)

Set Implicit Arguments.

mathink

(* -*- mode: coq -*- *)
(* Time-stamp: <2014/9/6 22:44:0> *)
(*
  Scratch.v 
  - mathink : Author
 *)

(** * Category Theory 'on' Coq *)