ivor-0.1.5: examplett/fin.tt

Load "lt.tt";

Data Fin : (n:Nat)* where
      fz : (k:Nat)(Fin (S k))
    | fs : (k:Nat)(i:Fin k)(Fin (S k));

mkFin : (m,n:Nat)(p:Lt m n)(Fin n);
intros;
induction p;
intros;
refine fz;
intros;
refine fs;
fill p_IH;
Qed;