| id fun x => x : ?m → ?m | |
| 0 : Nat | |
| f 1 fun x => x : Nat | |
| 0 : Nat | |
| f 1 fun x => x : Nat | |
| id.{u} {α : Sort u} (a : α) : α | |
| precissues.lean:15:10-15:14: error: unexpected token 'have'; expected command | |
| id.{u} {α : Sort u} (a : α) : α | |
| precissues.lean:17:10-17:13: error: unexpected token 'let'; expected command | |
| 1 : Nat | |
| id | |
| (let_fun this := True.intro; | |
| this) : True | |
| 0 = | |
| let_fun this := 1; | |
| this : Prop | |
| 0 = | |
| let x := 0; | |
| x : Prop | |
| p ↔ ¬q : Prop | |
| True = ¬False : Prop | |
| p ∧ ¬q : Prop | |
| ¬p ∧ q : Prop | |
| ¬p ↔ q : Prop | |
| ¬p = q : Prop | |
| ¬p = q : Prop | |
| id ¬p : Prop | |
| Nat → ∀ (a : Nat), a = a : Prop | |
| id.{u} {α : Sort u} (a : α) : α | |
| precissues.lean:41:10-41:14: error: unexpected token 'foo!'; expected command |