Matrix transposition: Difference between revisions

no edit summary
No edit summary
Line 90:
0.30 0.70 1.10
</pre>
 
=={{header|Agda}}==
<lang agda>module Matrix where
 
open import Data.Nat
open import Data.Vec
 
Matrix : (A : Set) → ℕ → ℕ → Set
Matrix A m n = Vec (Vec A m) n
 
transpose : ∀ {A m n} → Matrix A m n → Matrix A n m
transpose [] = replicate []
transpose (xs ∷ xss) = zipWith _∷_ xs (transpose xss)
 
a = (1 ∷ 2 ∷ 3 ∷ []) ∷ (4 ∷ 5 ∷ 6 ∷ []) ∷ []
b = transpose a</lang>
 
'''b''' evaluates to the following normal form:
 
<lang agda>(1 ∷ 4 ∷ []) ∷ (2 ∷ 5 ∷ []) ∷ (3 ∷ 6 ∷ []) ∷ []</lang>
 
=={{header|ALGOL 68}}==
Anonymous user