MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "relevantArgErasedMagicVec.ma" ---
--- scope checking ---
--- type checking ---
type  Sigma : ^(A : Set) -> ^(B : A -> Set) -> Set
term  Sigma.pair : .[A : Set] -> .[B : A -> Set] -> ^(fst : A) -> ^(snd : B fst) -> < Sigma.pair fst snd : Sigma A B >
term  fst : .[A : Set] -> .[B : A -> Set] -> (pair : Sigma A B) -> A
{ fst [A] [B] (Sigma.pair #fst #snd) = #fst
}
term  snd : .[A : Set] -> .[B : A -> Set] -> (pair : Sigma A B) -> B (fst [A] [B] pair)
{ snd [A] [B] (Sigma.pair #fst #snd) = #snd
}
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat >
type  Empty : Set
term  magic : .[A : Set] -> .[p : Empty] -> A
{}
type  Unit : Set
term  Unit.unit : < Unit.unit : Unit >
type  Vec : .[A : Set] -> (n : Nat) -> Set
error during typechecking:
Vec
/// clause 2
/// right hand side
/// checkExpr 2 |- Sigma A (\ z -> Vec A n) : Set
/// inferExpr' Sigma A (\ z -> Vec A n)
/// inferExpr' Sigma A
/// checkApp (^(A : Set) -> ^(B : A -> Set) -> Set) eliminated by A
/// inferExpr' A
/// inferExpr: variable A : Set may not occur
/// , because it is marked as erased