Commit 764e27d2 authored by Gaspard Ferey's avatar Gaspard Ferey

Minimalised an example.

parent bced5a29
A : Type.
a : A.
b : A.
def T : A -> Type.
def C : (x : A) -> T x -> Type.
[] C b _ --> A.
[] C a _ --> A.
(; This rule needs itself to type-check, since a must be in T b,
which is true if T b --> C b a --> A but not without any rule to define T ;)
[] T b --> C b a.
(; This rule needs itself to type-check, since a must be of type T a,
which is true if T a --> C a a --> A but not without any rule to define T ;)
[] T a --> C a a.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment