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 (2 lines) | stat: -rw-r--r-- 999 bytes parent folder | download 
1
2
 
Data.List.Base.map : Π ({A.a} : Agda.Primitive.Level) (Π ({A} : (Set (var 0))) (Π ({B.b} : Agda.Primitive.Level) (Π ({B} : (Set (var 0))) (Π (_ : (Π (_ : (var 2)) (var 1))) (Π (_ : (Agda.Builtin.List.List {var 4} (var 3))) (Agda.Builtin.List.List {var 3} (var 2)))))))
Data.List.Base.map = function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(f : Π (_ : (var 2)) (var 1)) ] {pat-var 4} {pat-var 3} {pat-var 2} {pat-var 1} pat-var 0 Agda.Builtin.List.List.[] → Agda.Builtin.List.List.[] {unknown} {unknown} ; [ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(f : Π (_ : (var 2)) (var 1))(x : var 3)(xs : Agda.Builtin.List.List {var 5} (var 4)) ] {pat-var 6} {pat-var 5} {pat-var 4} {pat-var 3} pat-var 2 (Agda.Builtin.List.List._∷_ pat-var 1 pat-var 0) → Agda.Builtin.List.List._∷_ {unknown} {unknown} (var 2 (var 1)) (Data.List.Base.map {var 6} {var 5} {var 4} {var 3} (var 2) (var 0)) ;}