Commit c6588468 authored by Francois THIRE's avatar Francois THIRE

n_vectors

parent a5ec0150
nat : Type.
0 : nat.
S : nat -> nat.
def A : Type.
vect : nat -> Type.
nil : vect 0.
cons : n : nat -> A -> vect n -> vect (S n).
def diag : nat -> nat -> Type.
[i] diag i 0 --> vect i.
[i,j] diag i (S j) --> A -> diag i j.
def c : n : nat -> diag n n.
def c' : n : nat -> m : nat -> A -> diag n m -> diag (S n) m.
[] c 0 --> nil.
[i,a] c (S i) a --> c' i i a (c i).
[n,a,v] c' n 0 a v --> cons n a v.
[n,m,a,v,b] c' n (S m) a v b --> c' n m a (v b).
def 1 : nat := S 0.
def 2 : nat := S 1.
def 3 : nat := S 2.
def 4 : nat := S 3.
def 5 : nat := S 4.
def 6 : nat := S 5.
x : A.
y : A.
w : A.
z : A.
#EVAL c 4 x y w z.
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