blob: 714e4e069f1d4d42e2c1641100bbbae6081d8e1f [file] [edit]
x y : Nat
h : x + 1 = 0
⊢ False
delta.lean:9:2-9:9: error: tactic 'delta' failed, did not delta reduce [f]
x y : Nat
h : f x = 0
⊢ False
delta.lean:12:2-12:15: error: tactic 'delta' failed, did not delta reduce [f] at h2
x y : Nat
h1 : f x = 0
h2 : 0 = 0
⊢ False
delta.lean:15:2-15:18: error: tactic 'delta' failed, did not delta reduce [f] at h2
x y : Nat
h1 : x + 1 = 0
h2 : 0 = 0
⊢ False
x y : Nat
h1 : x + 1 = 0
h2 : 0 = 0
⊢ False
delta.lean:23:2-23:14: error: tactic 'delta' failed, did not delta reduce [f]
x y : Nat
h2 : 0 = 0
⊢ False