MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "LowerSemiCont.ma" ---
--- scope checking ---
--- type checking ---
type  sup : (F : Size -> Set) -> +(i : Size) -> Set
{ sup F i = .[j < i] & F j
}
term  pairF : .[F : - Size -> Set] -> (a : F #) -> sup F #
term  pairF = [\ F ->] \ a -> ([#] , a)
term  supsup : .[F : Size -> Set] -> (a : sup F #) -> sup (sup F) #
term  supsup = [\ F ->] \ a -> ([#] , a)
type  bsup : (F : Size -> Set) -> +(i : Size) -> Set
{ bsup F i = .[j <= i] & F j
}
term  bsupsup : .[F : Size -> Set] -> (a : sup F #) -> bsup (sup F) #
term  bsupsup = [\ F ->] \ a -> ([#] , a)
type  SNat : + Size -> Set
term  SNat.szero : .[s!ze : Size] -> .[i < s!ze] -> SNat s!ze
term  SNat.szero : .[i : Size] -> < SNat.szero i : SNat $i >
term  SNat.ssuc : .[s!ze : Size] -> .[i < s!ze] -> ^ SNat i -> SNat s!ze
term  SNat.ssuc : .[i : Size] -> ^(y1 : SNat i) -> < SNat.ssuc i y1 : SNat $i >
term  pairSNat : (a : SNat #) -> .[j < #] & SNat j
term  pairSNat = \ a -> ([#] , a)
term  pairSNat2 : (a : SNat #) -> .[j < #] & SNat j & SNat j
term  pairSNat2 = \ a -> ([#] , (a , a))
type  Fork : ++(A : Set) -> Set
term  Fork.fork : .[A : Set] -> ^(fst : A) -> ^(snd : A) -> < Fork.fork fst snd : Fork A >
term  fst : .[A : Set] -> (fork : Fork A) -> A
{ fst [A] (Fork.fork #fst #snd) = #fst
}
term  snd : .[A : Set] -> (fork : Fork A) -> A
{ snd [A] (Fork.fork #fst #snd) = #snd
}
term  forkSNat : (a : SNat #) -> .[j < #] & Fork (SNat j)
term  forkSNat = \ a -> ([#] , Fork.fork a a)
type  Maybe : ++(A : Set) -> Set
term  Maybe.nothing : .[A : Set] -> < Maybe.nothing : Maybe A >
term  Maybe.just : .[A : Set] -> ^(fromJust : A) -> < Maybe.just fromJust : Maybe A >
term  maybeSNat : (a : SNat #) -> .[j < #] & Maybe (SNat j)
term  maybeSNat = \ a -> ([#] , Maybe.just a)
type  List : ++(A : Set) -> Set
term  List.nil : .[A : Set] -> < List.nil : List A >
term  List.cons : .[A : Set] -> ^(x : A) -> ^(xs : List A) -> < List.cons x xs : List A >
block fails as expected, error message:
listSNat
/// new a : (SNat #)
/// checkExpr 1 |- (# , cons a nil) : .[j < #] & List (SNat j)
/// checkForced fromList [(a,0)] |- (# , cons a nil) : .[j < #] & List (SNat j)
/// checkExpr 1 |- # : < #
/// leqVal' (subtyping)  < # : Size >  <=+  < #
/// leSize # <+ #
/// leSize: # < # failed
type  Nat : +(i : Size) -> Set
term  Nat.zero : .[i : Size] -> < Nat.zero : Nat i >
term  Nat.suc : .[i : Size] -> ^(jn : .[j < i] & Nat j) -> < Nat.suc jn : Nat i >
term  one : Nat #
term  one = Nat.suc ([#] , Nat.zero)
--- evaluating ---
--- closing "LowerSemiCont.ma" ---