leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4
https://leanprover.github.io/theorem_proving_in_lean4/
Apache License 2.0
164 stars 93 forks source link

Changed #check to #print in misused circumstances #5

Closed TimeTravelPenguin closed 3 years ago

TimeTravelPenguin commented 3 years ago

For example, given:

variable {p : Prop}
variable {q : Prop}
theorem t1 (hp : p) (hq : q) : p := hp

#check t1 yields: t1 : ?m.57 → ?m.58 → ?m.571

#print t1 yields:

theorem Demo.t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp