Agda.TypeChecking.Abstract

abstractType r a v b[v] = b where a : v.

piAbstractTerm NotHidden v a b[v] = (w : a) -> b[w] piAbstractTerm Hidden v a b[v] = {w : a} -> b[w]

piAbstract (v, a) b[v] = (w : a) -> b[w]

For the inspect idiom, it does something special: @piAbstract (v, a) b[v] = (w : a) {w' : Eq a w v} -> b[w]

For rewrite, it does something special: piAbstract (prf, Eq a v v') b[v,prf] = (w : a) (w' : Eq a w v') -> b[w,w']

isPrefixOf u v = Just es if v == u applyE es.

This swaps var 0 and var 1.