File: expected

package info (click to toggle)
agda-stdlib 2.1-4
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 9,196 kB
  • sloc: haskell: 375; makefile: 32; sh: 28; lisp: 1
file content (5 lines) | stat: -rw-r--r-- 1,313 bytes parent folder | download 
1
2
3
4
5
 
function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(x : var 2)(y : var 1) ] {pat-var 5} {pat-var 4} {pat-var 3} {pat-var 2} pat-var 1 pat-var 0 → var 0 ;}
function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(x : var 2)(y : var 1) ] {pat-var 5} {pat-var 4} {pat-var 3} {pat-var 2} pat-var 1 pat-var 0 → var 1 ;}
function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(x : var 2)(y : var 1)(z : var 2) ] {pat-var 6} {pat-var 5} {pat-var 4} {pat-var 3} pat-var 2 pat-var 1 pat-var 0 → var 2 ;}
function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(x : Agda.Builtin.List.List {Agda.Primitive._⊔_ (var 3) (var 1)} (Π (_ : (var 2)) (var 1)))(y : var 3)(z : var 2)(a : var 3) ] {pat-var 7} {pat-var 6} {pat-var 5} {pat-var 4} pat-var 3 pat-var 2 pat-var 1 pat-var 0 → var 3 ;}
function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(x : Π (_ : (var 2)) (Agda.Builtin.List.List {var 2} (var 1)))(y : var 3)(z : var 2)(a : Agda.Builtin.List.List {var 4} (var 3)) ] {pat-var 7} {pat-var 6} {pat-var 5} {pat-var 4} pat-var 3 pat-var 2 pat-var 1 pat-var 0 → var 3 ;}