
  0 | module Stellar.API.Telescope
  1 | 
  2 | import Data.Telescope
  3 | import Stellar.API
  4 | 
  5 | namespace Right
  6 | 
  7 |   public export
  8 |   Tele : Right.Telescope (S n) -> API
  9 |   Tele (x .- xs) = (v : x) !> Environment (xs v)
 10 | 
 11 | namespace Left
 12 | 
 13 |   public export
 14 |   Tele : Left.Telescope (S n) -> API
 15 |   Tele (x -. xs) = (v : Environment x) !> xs v
 16 | 
 17 | namespace Tree
 18 | 
 19 |   public export
 20 |   Tele : Tree.Telescope n -> API
 21 |   Tele [] = End
 22 |   Tele (Elt x) = x :- Unit
 23 |   Tele (gamma >< delta) = (v : Environment gamma) !> Environment (delta v)
 24 | 
 25 |