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

chore: use #lang lean4

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-14 17:30:26 -07:00
parent 94ea1dc705
commit 3b34a150ff
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/App.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -7,7 +8,6 @@ import Lean.Util.FindMVar
import Lean.Elab.Term
import Lean.Elab.Binders
import Lean.Elab.SyntheticMVars
new_frontend
namespace Lean.Elab.Term
open Meta