------------------------------------------------------------------------
-- The Agda standard library
--
-- Fancy display functions for Vec-based tables
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
module Text.Tabular.Vec where
open import Data.List.Base using (List)
open import Data.Product.Base as Prod using (uncurry)
open import Data.String using (String; rectangle; fromAlignment)
open import Data.Vec.Base
open import Function.Base
open import Text.Tabular.Base
display : ∀ {m n} → TabularConfig → Vec Alignment n → Vec (Vec String n) m →
List String
display c a = unsafeDisplay c
∘ toList
∘ map toList
∘ transpose
∘ map (uncurry rectangle ∘ unzip)
∘ transpose
∘ map (zip (map fromAlignment a))
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4