max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-08 15:52:55 -07:00
parent 50363b9267
commit d4d4e199bc
1 changed files with 0 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Lean/Elab/Binders.lean
View file

@ -433,14 +433,6 @@ withLetDecl ref n type val $ fun x => do
body ← instantiateMVars ref body;
mkLet ref x body
def elabLetIdDecl (ref : Syntax) (decl body : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
-- `decl` is of the form: ident bracktedBinder+ (`:` term)? `:=` term
let n := decl.getIdAt 0;
let binders := (decl.getArg 1).getArgs;
let type := expandOptType ref (decl.getArg 2);
let val := decl.getArg 4;
elabLetDeclAux ref n binders type val body expectedType?
@[builtinTermElab «let»] def elabLetDecl : TermElab :=
fun stx expectedType? => match_syntax stx with
| `(let $id:ident $args* := $val; $body) =>