bobatkey

{-# OPTIONS --postfix-projections #-}

module tuple where





------------------------------------------------------------------------------
--

jldodds

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Lists.List.
Import ListNotations.

Open Scope string_scope.

(* Make it print lists one item per line*)
Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..))
  (format "[ '[' x ;  '//' y ;  '//' .. ;  '//' z ']' ]") : list_scope.

Keno

graninas

Haskeller Competency Matrix

See also List of materials about Software Design in Haskell

	Junior	Middle	Senior	Architect
Haskell level	Basic Haskell	Intermediate Haskell	Advanced Haskell	Language-agnostic
Haskell knowledge scope	Learn you a Haskell	Get programming with Haskell	Haskell in Depth	Knows several languages from different categories
	Get programming with Haskell	Haskell in Depth	Functional Design and Architecture
			[Other books on Software Engineering in Haskell](https://github.com/graninas/software-design-in-haskell#B

amintimany

Require Import Coq.Logic.JMeq.

Definition JMeq_eq := forall (A : Type) (x y : A), JMeq x y -> x = y.

Section Eq_Facts.
  Variable A : Type.

  Definition K := forall (x : A) (P : x = x -> Prop), P eq_refl -> forall (eq : x = x), P eq.

  Definition URIP := forall (x : A) (eq : x = x), eq = eq_refl.