-- This file:
--   http://anggtwu.net/LEAN/telescopes1.lean.html
--   http://anggtwu.net/LEAN/telescopes1.lean
--          (find-angg "LEAN/telescopes1.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LEAN/telescopes1.lean"))
-- (find-es "agda" "telescopes")
-- (find-es "agda" "variable")
-- (find-es "lean" "variable")
-- (find-es "lean" "telescopes")


variable (A : Type)
variable (a : A)
variable (B : A → Type)
variable (b : B a)
variable (C : (a : A) → (b : B a) → Type)


def foo (a : A) := 42
-- def foo3 (a : A) (b : B a) (c : C a b) := sorry


-- 







-- Local Variables:
-- coding:  utf-8-unix
-- End: