tests/lean/4375.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            example: Nat → Nat :=

            
              let a : Nat := Nat.zero

            
              fun (_ : Nat) =>

            
                let b : Nat := Nat.zero

            
                (fun (_ : a = b) => 0) (Eq.refl a)
	example: Nat → Nat :=
	let a : Nat := Nat.zero
	fun (_ : Nat) =>
	let b : Nat := Nat.zero
	(fun (_ : a = b) => 0) (Eq.refl a)