| inductionGen.lean:23:2-23:14: error: index in target's type is not a variable (consider using the `cases` tactic instead) | |
| n + 1 | |
| inductionGen.lean:25:8-25:11: warning: declaration uses 'sorry' | |
| case cons | |
| α : Type u_1 | |
| n : Nat | |
| ys : Vec α (n + 1) | |
| x : α | |
| xs : Vec α n | |
| h : Vec.cons x xs = ys | |
| ⊢ Vec.head (Vec.cons x xs) = Vec.head ys | |
| inductionGen.lean:64:8-64:11: warning: declaration uses 'sorry' | |
| case natVal | |
| α : ExprType | |
| a✝ : Nat | |
| b : Expr ExprType.nat | |
| h : Expr.natVal a✝ = b | |
| ⊢ eval (constProp (Expr.natVal a✝)) = eval b | |
| case boolVal | |
| α : ExprType | |
| a✝ : Bool | |
| b : Expr ExprType.bool | |
| h : Expr.boolVal a✝ = b | |
| ⊢ eval (constProp (Expr.boolVal a✝)) = eval b | |
| case eq | |
| α α✝ : ExprType | |
| a✝¹ a✝ : Expr α✝ | |
| a_ih✝¹ : ∀ (b : Expr α✝), a✝¹ = b → eval (constProp a✝¹) = eval b | |
| a_ih✝ : ∀ (b : Expr α✝), a✝ = b → eval (constProp a✝) = eval b | |
| b : Expr ExprType.bool | |
| h : Expr.eq a✝¹ a✝ = b | |
| ⊢ eval (constProp (Expr.eq a✝¹ a✝)) = eval b | |
| case add | |
| α : ExprType | |
| a✝¹ a✝ : Expr ExprType.nat | |
| a_ih✝¹ : ∀ (b : Expr ExprType.nat), a✝¹ = b → eval (constProp a✝¹) = eval b | |
| a_ih✝ : ∀ (b : Expr ExprType.nat), a✝ = b → eval (constProp a✝) = eval b | |
| b : Expr ExprType.nat | |
| h : Expr.add a✝¹ a✝ = b | |
| ⊢ eval (constProp (Expr.add a✝¹ a✝)) = eval b | |
| inductionGen.lean:78:2-78:27: error: target (or one of its indices) occurs more than once | |
| n |