MiniAgda by Andreas Abel and Karl Mehltretter --- opening "bfTypeNotAdmissible.ma" --- --- scope checking --- --- type checking --- type Prod : ++(A : Set) -> ++(B : Set) -> Set term Prod.pair : .[A : Set] -> .[B : Set] -> ^(y0 : A) -> ^(y1 : B) -> < Prod.pair y0 y1 : Prod A B > term split : .[A : Set] -> .[B : Set] -> Prod A B -> .[C : Set] -> (A -> B -> C) -> C { split [A] [B] (Prod.pair a b) [C] f = f a b } type List : ++(A : Set) -> + Size -> Set term List.nil : .[A : Set] -> .[s!ze : Size] -> .[i < s!ze] -> List A s!ze term List.nil : .[A : Set] -> .[i : Size] -> < List.nil i : List A $i > term List.cons : .[A : Set] -> .[s!ze : Size] -> .[i < s!ze] -> ^ A -> ^ List A i -> List A s!ze term List.cons : .[A : Set] -> .[i : Size] -> ^(y1 : A) -> ^(y2 : List A i) -> < List.cons i y1 y2 : List A $i > term append : .[A : Set] -> List A # -> List A # -> List A # { append [A] (List.nil [.#]) l = l ; append [A] (List.cons [.#] a as) l = List.cons [#] a (append [A] as l) } type Rose : ++(A : Set) -> + Size -> Set term Rose.rose : .[A : Set] -> .[s!ze : Size] -> .[i < s!ze] -> ^ A -> ^ List (Rose A i) # -> Rose A s!ze term Rose.rose : .[A : Set] -> .[i : Size] -> ^(y1 : A) -> ^(y2 : List (Rose A i) #) -> < Rose.rose i y1 y2 : Rose A $i > term step : .[j : Size] -> .[A : Set] -> .[i : Size] -> List (Rose A $i) j -> Prod (List A j) (List (Rose A i) #) { step [.$j] [A] [i] (List.nil [j]) = Prod.pair (List.nil [j]) (List.nil [#]) ; step [.$j] [A] [.i] (List.cons [j] (Rose.rose [i] a rs') rs) = split [List A j] [List (Rose A i) #] (step [j] [A] [i] rs) [Prod (List A $j) (List (Rose A i) #)] (\ as -> \ rs'' -> Prod.pair (List.cons [j] a as) (append [Rose A i] rs' rs'')) } term bf' : .[A : Set] -> .[i : Size] -> List A # -> List (Rose A i) # -> List A # error during typechecking: checking type of bf' for admissibility /// new A : _ /// new as : _ /// new i : _ /// new a : _ /// new r : _ /// new rs : _ /// new i <= # /// admType: checking ((List v0 #)::Tm -> {List (Rose A i) # -> List A # {i = v6, A = v0}}) admissible in v6 /// new : (List v0 #) /// admType: checking ((List {Rose A i {i = v6, A = v0}} #)::Tm -> {List A # {i = v6, A = v0}}) admissible in v6 /// type List (Rose A i) # not lower semi continuous in i