module Chapter5.IDesc.Examples.ToIDesc where open import Level renaming ( zero to zeroL ; suc to sucL) open import Data.Unit open import Data.Nat open import Data.Fin open import Chapter4.Desc open import Chapter5.IDesc toIDesc : (D : Desc zeroL) → IDesc zeroL ⊤ toIDesc `var = `var tt toIDesc `1 = `1 toIDesc (D `× D') = toIDesc D `× toIDesc D' toIDesc (D `+ D') = `σ 2 λ { zero → toIDesc D ; (suc zero) → toIDesc D' ; (suc (suc ())) } toIDesc (`Σ S T) = `Σ S λ s → toIDesc (T s) toIDesc (`Π S T) = `Π S λ s → toIDesc (T s)