MiniAgda by Andreas Abel and Karl Mehltretter --- opening "AccDestructorErasedIndex.ma" --- --- scope checking --- --- type checking --- type Nat : Set term Nat.zero : < Nat.zero : Nat > term Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat > type R : ^ Nat -> ^ Nat -> Set term R.r1 : .[x : Nat] -> < R.r1 x : R (Nat.succ (Nat.succ x)) (Nat.succ Nat.zero) > term R.r2 : < R.r2 : R (Nat.succ Nat.zero) Nat.zero > type Acc : ^(A : Set) -> ^(Lt : A -> A -> Set) -> (b : A) -> Set term Acc.acc : .[A : Set] -> .[Lt : A -> A -> Set] -> .[b : A] -> ^(accParOut : (a : A) -> Lt a b -> Acc A Lt a) -> < Acc.acc accParOut : Acc A Lt b > term accParOut : .[A : Set] -> .[Lt : A -> A -> Set] -> (b : A) -> (acc : Acc A Lt b) -> (a : A) -> Lt a b -> Acc A Lt a { accParOut [A] [Lt] b (Acc.acc #accParOut) = #accParOut } term acc_dest : (n : Nat) -> (p : Acc Nat R n) -> (m : Nat) -> R m n -> Acc Nat R m { acc_dest n (Acc.acc p) = p } term acc2 : (n : Nat) -> Acc Nat R (Nat.succ (Nat.succ n)) term acc2 = \ n -> Acc.acc (\ a -> \ p -> case p : R a (Nat.succ (Nat.succ n)) {}) term aux1 : (a : Nat) -> (p : R a (Nat.succ Nat.zero)) -> Acc Nat R a { aux1 (Nat.succ (Nat.succ x)) (R.r1 [.x]) = acc2 x } term acc1 : Acc Nat R (Nat.succ Nat.zero) term acc1 = Acc.acc aux1 term aux0 : (a : Nat) -> (p : R a Nat.zero) -> Acc Nat R a { aux0 .(succ zero) R.r2 = acc1 } term acc0 : Acc Nat R Nat.zero term acc0 = Acc.acc aux0 term accR : (n : Nat) -> Acc Nat R n { accR Nat.zero = acc0 ; accR (Nat.succ Nat.zero) = acc1 ; accR (Nat.succ (Nat.succ n)) = acc2 n } term f : (x : Nat) -> Acc Nat R x -> Nat { f x (Acc.acc p) = case x : Nat { Nat.zero -> f (Nat.succ x) (p (Nat.succ x) R.r2) ; Nat.succ Nat.zero -> f (Nat.succ x) (p (Nat.succ x) (R.r1 [Nat.zero])) ; Nat.succ (Nat.succ y) -> Nat.zero } } term h : (x : Nat) -> .[Acc Nat R x] -> Nat { h Nat.zero [Acc.acc [p]] = h (Nat.succ Nat.zero) [p (Nat.succ Nat.zero) R.r2] ; h (Nat.succ Nat.zero) [Acc.acc [p]] = h (Nat.succ (Nat.succ Nat.zero)) [p (Nat.succ (Nat.succ Nat.zero)) (R.r1 [Nat.zero])] ; h (Nat.succ (Nat.succ y)) [p] = Nat.zero } term bla : Nat term bla = h Nat.zero [acc0] type Id : ^(A : Set) -> ^(a : A) -> ^ A -> Set term Id.refl : .[A : Set] -> .[a : A] -> < Id.refl : Id A a a > block fails as expected, error message: p1 /// checkExpr 0 |- \ p -> refl : (p : Acc Nat R Nat.zero) -> Id Nat (h Nat.zero [p]) (h Nat.zero [acc0]) /// checkForced fromList [] |- \ p -> refl : (p : Acc Nat R Nat.zero) -> Id Nat (h Nat.zero [p]) (h Nat.zero [acc0]) /// new p : (Acc Nat R Nat.zero) /// checkExpr 1 |- refl : Id Nat (h Nat.zero [p]) (h Nat.zero [acc0]) /// checkForced fromList [(p,0)] |- refl : Id Nat (h Nat.zero [p]) (h Nat.zero [acc0]) /// leqVal' (subtyping) < Id.refl : Id Nat (h Nat.zero [p]) (h Nat.zero [p]) > <=+ Id Nat (h Nat.zero [p]) (h Nat.zero [acc0]) /// leqVal' (subtyping) Id Nat (h Nat.zero [p]) (h Nat.zero [p]) <=+ Id Nat (h Nat.zero [p]) (h Nat.zero [acc0]) /// leqVal' h Nat.zero p <=^ Nat.zero : Nat /// leqApp: head mismatch h != Nat.zero --- evaluating --- acc0 has whnf (acc (aux0 Up ((a : Nat::Tm) -> (p : R a Nat.zero) -> Acc Nat R a))) acc0 evaluates to acc (\ a~0 -> \ p~1 -> aux0 ~0 ~1) bla has whnf (h zero acc0) bla evaluates to h zero (Acc.acc (\ a~0 -> \ p~1 -> aux0 ~0 ~1)) --- closing "AccDestructorErasedIndex.ma" ---