comments

encodings/deptype.lp

 /// Dependent types
 
 /// PVS allows dependent types using theory abstraction. For instance,
-/// vector[t: TYPE, n: nat]: THEORY BEGIN vec: TYPE END vector
+/// vector_real[n: nat]: THEORY BEGIN vec: TYPE END vector
 /// allows to define
-/// cons(n: nat, e: t, v: vector[t, n].vec): vector[t, n + 1].vec
+/// cons(n: nat, r: real, v: vector_real[n].vec): vector_real[n + 1].vec
 
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert