| 440.lean:1:21-1:22: error: don't know how to synthesize placeholder | |
| context: | |
| ⊢ True | |
| 440.lean:4:29-4:30: error: don't know how to synthesize placeholder | |
| context: | |
| x : Nat | |
| ⊢ Nat | |
| f (x : Nat) : Nat | |
| 440.lean:11:0-11:5: error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes. | |
| To attempt to evaluate anyway despite the risks, use the '#eval!' command. |