ichistmeinname

Set Implicit Arguments.

Inductive Simple (A: Type) := simple : Simple A.
Inductive Wrap (A: Type) :=
| wrap : A -> Wrap A
| funWrap : forall X, Simple X -> (X -> Wrap A) -> Wrap A.

Definition anotherWrap A : Wrap A :=
  funWrap (simple A) (fun x => wrap x).

ichistmeinname

Require Import Lists.List.
Require Import Arith.Arith.

Require Import Omega.

Set Implicit Arguments.

Fixpoint replicate A (n : nat) (x : A) : list A :=
  match n with
  | O => nil

ichistmeinname

--------------------------------
-- Pretty Printing type class --
--------------------------------

class Pretty a where
  pretty :: a -> String
  pprint :: a -> IO ()
  pprint = putStrLn . pretty 

instance Pretty Int where

ichistmeinname

(* The following two examples fulfill the (strict) positivity condition *)

Inductive Switch (A : Type) : Type :=
| switch : Switch A -> Switch A.

Inductive UseSwitch :=
| useSwitch : Switch UseSwitch -> UseSwitch.
 

Inductive SwitchSP (A : Type) : Type :=