chore: move to new frontend

src/Lean/Meta/Offset.lean

@@ -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.
@@ -6,43 +7,43 @@ Authors: Leonardo de Moura
 import Lean.Data.LBool
 import Lean.Meta.InferType
 
-namespace Lean
-namespace Meta
+namespace Lean.Meta
 
 partial def evalNat : Expr → Option Nat
 | Expr.lit (Literal.natVal n) _ => pure n
 | Expr.mdata _ e _              => evalNat e
 | Expr.const `Nat.zero _ _      => pure 0
-| e@(Expr.app _ a _)            =>
-  let fn    := e.getAppFn;
+| e@(Expr.app _ a _)            => do
+  let fn    := e.getAppFn
   match fn with
   | Expr.const c _ _ =>
-    let nargs := e.getAppNumArgs;
-    if c == `Nat.succ && nargs == 1 then do
-      v ← evalNat a; pure $ v+1
-    else if c == `Nat.add && nargs == 2 then do
-      v₁ ← evalNat (e.getArg! 0);
-      v₂ ← evalNat (e.getArg! 1);
+    let nargs := e.getAppNumArgs
+    if c == `Nat.succ && nargs == 1 then
+      let v ← evalNat a
+      pure $ v+1
+    else if c == `Nat.add && nargs == 2 then
+      let v₁ ← evalNat (e.getArg! 0)
+      let v₂ ← evalNat (e.getArg! 1)
       pure $ v₁ + v₂
-    else if c == `Nat.sub && nargs == 2 then do
-      v₁ ← evalNat (e.getArg! 0);
-      v₂ ← evalNat (e.getArg! 1);
+    else if c == `Nat.sub && nargs == 2 then
+      let v₁ ← evalNat (e.getArg! 0)
+      let v₂ ← evalNat (e.getArg! 1)
       pure $ v₁ - v₂
-    else if c == `Nat.mul && nargs == 2 then do
-      v₁ ← evalNat (e.getArg! 0);
-      v₂ ← evalNat (e.getArg! 1);
+    else if c == `Nat.mul && nargs == 2 then
+      let v₁ ← evalNat (e.getArg! 0)
+      let v₂ ← evalNat (e.getArg! 1)
       pure $ v₁ * v₂
-    else if c == `HasAdd.add && nargs == 4 then do
-      v₁ ← evalNat (e.getArg! 2);
-      v₂ ← evalNat (e.getArg! 3);
+    else if c == `HasAdd.add && nargs == 4 then
+      let v₁ ← evalNat (e.getArg! 2)
+      let v₂ ← evalNat (e.getArg! 3)
       pure $ v₁ + v₂
-    else if c == `HasAdd.sub && nargs == 4 then do
-      v₁ ← evalNat (e.getArg! 2);
-      v₂ ← evalNat (e.getArg! 3);
+    else if c == `HasAdd.sub && nargs == 4 then
+      let v₁ ← evalNat (e.getArg! 2)
+      let v₂ ← evalNat (e.getArg! 3)
       pure $ v₁ - v₂
-    else if c == `HasAdd.mul && nargs == 4 then do
-      v₁ ← evalNat (e.getArg! 2);
-      v₂ ← evalNat (e.getArg! 3);
+    else if c == `HasAdd.mul && nargs == 4 then
+      let v₁ ← evalNat (e.getArg! 2)
+      let v₂ ← evalNat (e.getArg! 3)
       pure $ v₁ * v₂
     else if c == `HasOfNat.ofNat && nargs == 3 then
       evalNat (e.getArg! 2)
@@ -54,20 +55,20 @@ partial def evalNat : Expr → Option Nat
 /- Quick function for converting `e` into `s + k` s.t. `e` is definitionally equal to `Nat.add s k`. -/
 private partial def getOffsetAux : Expr → Bool → Option (Expr × Nat)
 | e@(Expr.app _ a _), top =>
-  let fn := e.getAppFn;
+  let fn := e.getAppFn
   match fn with
   | Expr.const c _ _ =>
-    let nargs := e.getAppNumArgs;
+    let nargs := e.getAppNumArgs
     if c == `Nat.succ && nargs == 1 then do
-      (s, k) ← getOffsetAux a false;
+      let (s, k) ← getOffsetAux a false
       pure (s, k+1)
     else if c == `Nat.add && nargs == 2 then do
-      v      ← evalNat (e.getArg! 1);
-      (s, k) ← getOffsetAux (e.getArg! 0) false;
+      let v      ← evalNat (e.getArg! 1)
+      let (s, k) ← getOffsetAux (e.getArg! 0) false
       pure (s, k+v)
     else if c == `HasAdd.add && nargs == 4 then do
-      v      ← evalNat (e.getArg! 3);
-      (s, k) ← getOffsetAux (e.getArg! 2) false;
+      let v      ← evalNat (e.getArg! 3)
+      let (s, k) ← getOffsetAux (e.getArg! 2) false
       pure (s, k+v)
     else if top then none else pure (e, 0)
   | _ => if top then none else pure (e, 0)
@@ -78,10 +79,10 @@ getOffsetAux e true
 
 private partial def isOffset : Expr → Option (Expr × Nat)
 | e@(Expr.app _ a _) =>
-  let fn := e.getAppFn;
+  let fn := e.getAppFn
   match fn with
   | Expr.const c _ _ =>
-    let nargs := e.getAppNumArgs;
+    let nargs := e.getAppNumArgs
     if (c == `Nat.succ && nargs == 1) || (c == `Nat.add && nargs == 2) || (c == `HasAdd.add && nargs == 4) then
       getOffset e
     else none
@@ -99,7 +100,7 @@ else if isNatZero e then mkNatLit offset
 else mkAppB (mkConst `Nat.add) e (mkNatLit offset)
 
 def isDefEqOffset (s t : Expr) : DefEqM LBool :=
-let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
+let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t
 match isOffset s with
 | some (s, k₁) => match isOffset t with
   | some (t, k₂) => -- s+k₁ =?= t+k₂
@@ -119,5 +120,4 @@ match isOffset s with
       | none    => pure LBool.undef
   | none    => pure LBool.undef
 
-end Meta
-end Lean
+end Lean.Meta

src/Lean/Meta/Tactic.lean

@@ -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.

src/Lean/Meta/TransparencyMode.lean

@@ -1,10 +1,10 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-namespace Lean
-namespace Meta
+namespace Lean.Meta
 
 inductive TransparencyMode
 | all | default | reducible
@@ -35,5 +35,4 @@ def lt : TransparencyMode → TransparencyMode → Bool
 
 end TransparencyMode
 
-end Meta
-end Lean
+end Lean.Meta