
  0 | module Core.TT.Views
  1 | 
  2 | import Core.Env
  3 | import Core.TT
  4 | 
  5 | ||| Go under n Pis (if n < 0 then go under as many as possible)
  6 | export
  7 | underPis : (n : Int) -> Env Term vars -> Term vars ->
  8 |            (bnds : SnocList Name ** (Env Term (bnds <>> vars), Term (bnds <>> vars)))
  9 | underPis 0 env t = ([<] ** (env, t))
 10 | underPis n env (Bind fc x bd@(Pi {}) scope) =
 11 |   let (bnds ** (env', scope')) := underPis (n - 1) (bd :: env) scope in
 12 |   (bnds :< x ** (env', scope'))
 13 | underPis n env (Bind fc x bd@(PLet fc1 y val ty) scope) = underPis n env (subst val scope)
 14 | underPis n env t = ([<] ** (env, t))
 15 |