README

               	         THE IRRELEVANT COQ SYSTEM
            	         =========================

Take Coq.

Add in its syntax (up to kernel/extensions.ml) :
 - Irr : Type(0)
 - iPrf : Irr -> Prop
 - iJMeq : forall {A B: Type}, A -> B -> Irr
 - iSubst : forall {A: Type} (a: A) (b: A)
    (eq: iPrf (iJMeq a b)) (P : A -> Type) (p : P a), P b

Make it typecheck them (kernel/extension_behavior.ml +
kernel/typeops.ml).

Add in its conversion test (kernel/reduction.ml:ccnv) :
G |- p == q : forall (x_1: T_1) ... (x_n: T_n), iPrf A

Add in the reduction machine (kernel/closure.ml) :
      G |- a == b : A
____________________________
G |- isubst a b eq P p ==> p


Of course, Coq reduction machine and conversion test are not typed so
you have cheated by
 - carrying and updating a typing environment that destructs all the performance
 - declaring references "nasty_infer" & "nasty_conv" in kernel/closure.ml
that you set to the latter-defined functions afterward.

Of course, it is completely incomplete and will do "pattern matching
failure" if you try to use cbv reduction machines.

Of course, it is full of bugs such as the one that makes NMake_gen.v
kill your computer if you keep "reflexivity" instead of "exact
eq_refl" at some point. I personnaly stop the massacre after 30Go of
swap!

But at least, you will obtain a playground thus this one ... Sandbox
is open at theories/Irr/Irr.v.