Daten-abhängige Typen

(dependent types) - Typ ist anhängig von Daten,

in Agda (http://wiki.portal.chalmers.se/agda/)

data Nat : Set where 
    zero : Nat ; suc  : Nat -> Nat
Vec : Nat -> Set -> Set
vHead : {X : Set}->(n : Nat)->Vec (suc n) X -> X
transpose : {m n : Nat}{X : Set} 
   -> Vec m (Vec n X) -> Vec n (Vec m X)



Johannes Waldmann 2014-03-31