greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

remove mathlib as dependecy

Browse Source
This commit is contained in:
Jon Eugster
2023-05-08 18:23:18 +02:00
parent 471989d668
commit 0deb55e8ac
25 changed files with 464 additions and 52 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
NNG/Levels/Inequality/Level_10.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_11.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_12.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_13.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_14.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_15.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_16.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_17.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

6
NNG/Levels/Inequality/Level_3.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
import Std.Tactic.RCases
Game "NNG"
@@ -20,7 +20,7 @@ that the `cases` tactic can be used (just like it was used to extract
information from `∧` and `∨` and `↔` hypotheses). Let me talk you through
the proof of $a\\le b\\implies a\\le\\operatorname{succ}(b)$.
The goal is an implication so we clearly want to start with
The goal is an implication so we clearly want to start with
`intro h,`
@@ -43,7 +43,7 @@ Now use `use` wisely and you're home.
"
Statement
"For all naturals $a$, $b$, if $a\\leq b$ then $a\\leq \\operatorname{succ}(b)$.
"For all naturals $a$, $b$, if $a\\leq b$ then $a\\leq \\operatorname{succ}(b)$.
"
(a b : ℕ) : a ≤ b → a ≤ (succ b) := by
intro h

2
NNG/Levels/Inequality/Level_4.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_5.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_6.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_7.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_8.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

2
NNG/Levels/Inequality/Level_9.lean
View File

@@ -1,6 +1,6 @@
import NNG.Metadata
import NNG.MyNat.LE
import Mathlib.Tactic.Use
import NNG.Tactic.Use
Game "NNG"
World "Inequality"

6
NNG/Metadata.lean
View File

@@ -10,9 +10,9 @@ import NNG.Tactic.Induction
import NNG.Tactic.Rfl
import NNG.Tactic.Rw
import Std.Tactic.RCases
import Mathlib.Tactic.Have
import Mathlib.Tactic.LeftRight
import NNG.Tactic.Have
import NNG.Tactic.LeftRight
-- TODO: Why does this not work here??
-- We do not want `simp` to be able to do anything unless we unlock it manually.
attribute [-simp] MyNat.succ.injEq
attribute [-simp] MyNat.succ.injEq

67
NNG/Tactic/Have.lean Normal file
View File

@@ -0,0 +1,67 @@
/- copied from mathlib. -/
import Lean
-- import Mathlib.Data.Array.Defs
/--
Uses `checkColGt` to prevent
```lean
have h
exact Nat
```
From being interpreted as
```lean
have h
exact Nat
```
-/
def Lean.Parser.Term.haveIdLhs' : Parser :=
optional (ppSpace >> ident >> many (ppSpace >>
checkColGt "expected to be indented" >>
letIdBinder)) >> optType
namespace NNG.Tactic
open Lean Elab.Tactic Meta
syntax "have" Parser.Term.haveIdLhs' : tactic
syntax "let " Parser.Term.haveIdLhs' : tactic
syntax "suffices" Parser.Term.haveIdLhs' : tactic
open Elab Term in
def haveLetCore (goal : MVarId) (name : Option Syntax) (bis : Array Syntax)
(t : Option Syntax) (keepTerm : Bool) : TermElabM (MVarId × MVarId) :=
let declFn := if keepTerm then MVarId.define else MVarId.assert
goal.withContext do
let n := if let some n := name then n.getId else `this
let elabBinders k := if bis.isEmpty then k #[] else elabBinders bis k
let (goal1, t, p) ← elabBinders fun es ↦ do
let t ← match t with
| none => mkFreshTypeMVar
| some stx => withRef stx do
let e ← Term.elabTerm stx none
Term.synthesizeSyntheticMVars false
instantiateMVars e
let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque n
pure (p.mvarId!, ← mkForallFVars es t, ← mkLambdaFVars es p)
let (fvar, goal2) ← (← declFn goal n t p).intro1P
if let some stx := name then
goal2.withContext do
Term.addTermInfo' (isBinder := true) stx (mkFVar fvar)
pure (goal1, goal2)
elab_rules : tactic
| `(tactic| have $[$n:ident $bs*]? $[: $t:term]?) => do
let (goal1, goal2) ← haveLetCore (← getMainGoal) n (bs.getD #[]) t false
replaceMainGoal [goal1, goal2]
elab_rules : tactic
| `(tactic| suffices $[$n:ident $bs*]? $[: $t:term]?) => do
let (goal1, goal2) ← haveLetCore (← getMainGoal) n (bs.getD #[]) t false
replaceMainGoal [goal2, goal1]
elab_rules : tactic
| `(tactic| let $[$n:ident $bs*]? $[: $t:term]?) => withMainContext do
let (goal1, goal2) ← haveLetCore (← getMainGoal) n (bs.getD #[]) t true
replaceMainGoal [goal1, goal2]

5
NNG/Tactic/Induction.lean
View File

@@ -1,4 +1,4 @@
import Mathlib.Lean.Expr.Basic
import NNG.Tactic.LeanExprBasic
import Lean.Elab.Tactic.Basic
import NNG.MyNat.Definition
@@ -77,6 +77,3 @@ elab (name := _root_.MyNat.induction) "induction " tgts:(casesTarget,+)
setGoals <| (subgoals ++ result.others).toList ++ gs
end Lean.Parser.Tactic

342
NNG/Tactic/LeanExprBasic.lean Normal file
View File

@@ -0,0 +1,342 @@
/-
copied from mathlib
TODO: Just copied because some tactics depend on it,
probably can golf the copies of the mathlib tactics in
this game so that this isn't needed.
-/
import Lean
import Std.Lean.Expr
import Std.Data.List.Basic
/-!
# Additional operations on Expr and related types
This file defines basic operations on the types expr, name, declaration, level, environment.
This file is mostly for non-tactics.
-/
namespace Lean
namespace BinderInfo
/-! ### Declarations about `BinderInfo` -/
/-- The brackets corresponding to a given `BinderInfo`. -/
def brackets : BinderInfo → String × String
| BinderInfo.implicit => ("{", "}")
| BinderInfo.strictImplicit => ("{{", "}}")
| BinderInfo.instImplicit => ("[", "]")
| _ => ("(", ")")
end BinderInfo
namespace Name
/-! ### Declarations about `name` -/
/-- Find the largest prefix `n` of a `Name` such that `f n != none`, then replace this prefix
with the value of `f n`. -/
def mapPrefix (f : Name → Option Name) (n : Name) : Name := Id.run do
if let some n' := f n then return n'
match n with
| anonymous => anonymous
| str n' s => mkStr (mapPrefix f n') s
| num n' i => mkNum (mapPrefix f n') i
/-- Build a name from components. For example ``from_components [`foo, `bar]`` becomes
``` `foo.bar```.
It is the inverse of `Name.components` on list of names that have single components. -/
def fromComponents : List Name → Name := go .anonymous where
/-- Auxiliary for `Name.fromComponents` -/
go : Name → List Name → Name
| n, [] => n
| n, s :: rest => go (s.updatePrefix n) rest
/-- Update the last component of a name. -/
def updateLast (f : String → String) : Name → Name
| .str n s => .str n (f s)
| n => n
/-- Get the last field of a name as a string.
Doesn't raise an error when the last component is a numeric field. -/
def getString : Name → String
| .str _ s => s
| .num _ n => toString n
| .anonymous => ""
/-- `nm.splitAt n` splits a name `nm` in two parts, such that the *second* part has depth `n`, i.e.
`(nm.splitAt n).2.getNumParts = n` (assuming `nm.getNumParts ≥ n`).
Example: ``splitAt `foo.bar.baz.back.bat 1 = (`foo.bar.baz.back, `bat)``. -/
def splitAt (nm : Name) (n : Nat) : Name × Name :=
let (nm2, nm1) := (nm.componentsRev.splitAt n)
(.fromComponents <| nm1.reverse, .fromComponents <| nm2.reverse)
/-- `isPrefixOf? pre nm` returns `some post` if `nm = pre ++ post`.
Note that this includes the case where `nm` has multiple more namespaces.
If `pre` is not a prefix of `nm`, it returns `none`. -/
def isPrefixOf? (pre nm : Name) : Option Name :=
if pre == nm then
some anonymous
else match nm with
| anonymous => none
| num p' a => (isPrefixOf? pre p').map (·.num a)
| str p' s => (isPrefixOf? pre p').map (·.str s)
/-- Lean 4 makes declarations which are technically not internal
(that is, head string does not start with `_`) but which sometimes should
be treated as such. For example, the `to_additive` attribute needs to
transform `proof_1` constants generated by `Lean.Meta.mkAuxDefinitionFor`.
This might be better fixed in core, but until then, this method can act
as a polyfill. This method only looks at the name to decide whether it is probably internal.
Note: this declaration also occurs as `shouldIgnore` in the Lean 4 file `test/lean/run/printDecls`.
-/
def isInternal' (declName : Name) : Bool :=
declName.isInternal ||
match declName with
| .str _ s => "match_".isPrefixOf s || "proof_".isPrefixOf s || "eq_".isPrefixOf s
| _ => true
end Name
namespace ConstantInfo
/-- Checks whether this `ConstantInfo` is a definition, -/
def isDef : ConstantInfo → Bool
| defnInfo _ => true
| _ => false
/-- Checks whether this `ConstantInfo` is a theorem, -/
def isThm : ConstantInfo → Bool
| thmInfo _ => true
| _ => false
/-- Update `ConstantVal` (the data common to all constructors of `ConstantInfo`)
in a `ConstantInfo`. -/
def updateConstantVal : ConstantInfo → ConstantVal → ConstantInfo
| defnInfo info, v => defnInfo {info with toConstantVal := v}
| axiomInfo info, v => axiomInfo {info with toConstantVal := v}
| thmInfo info, v => thmInfo {info with toConstantVal := v}
| opaqueInfo info, v => opaqueInfo {info with toConstantVal := v}
| quotInfo info, v => quotInfo {info with toConstantVal := v}
| inductInfo info, v => inductInfo {info with toConstantVal := v}
| ctorInfo info, v => ctorInfo {info with toConstantVal := v}
| recInfo info, v => recInfo {info with toConstantVal := v}
/-- Update the name of a `ConstantInfo`. -/
def updateName (c : ConstantInfo) (name : Name) : ConstantInfo :=
c.updateConstantVal {c.toConstantVal with name}
/-- Update the type of a `ConstantInfo`. -/
def updateType (c : ConstantInfo) (type : Expr) : ConstantInfo :=
c.updateConstantVal {c.toConstantVal with type}
/-- Update the level parameters of a `ConstantInfo`. -/
def updateLevelParams (c : ConstantInfo) (levelParams : List Name) :
ConstantInfo :=
c.updateConstantVal {c.toConstantVal with levelParams}
/-- Update the value of a `ConstantInfo`, if it has one. -/
def updateValue : ConstantInfo → Expr → ConstantInfo
| defnInfo info, v => defnInfo {info with value := v}
| thmInfo info, v => thmInfo {info with value := v}
| opaqueInfo info, v => opaqueInfo {info with value := v}
| d, _ => d
/-- Turn a `ConstantInfo` into a declaration. -/
def toDeclaration! : ConstantInfo → Declaration
| defnInfo info => Declaration.defnDecl info
| thmInfo info => Declaration.thmDecl info
| axiomInfo info => Declaration.axiomDecl info
| opaqueInfo info => Declaration.opaqueDecl info
| quotInfo _ => panic! "toDeclaration for quotInfo not implemented"
| inductInfo _ => panic! "toDeclaration for inductInfo not implemented"
| ctorInfo _ => panic! "toDeclaration for ctorInfo not implemented"
| recInfo _ => panic! "toDeclaration for recInfo not implemented"
end ConstantInfo
open Meta
/-- Same as `mkConst`, but with fresh level metavariables. -/
def mkConst' (constName : Name) : MetaM Expr := do
return mkConst constName (← (← getConstInfo constName).levelParams.mapM fun _ => mkFreshLevelMVar)
namespace Expr
/-! ### Declarations about `Expr` -/
/-- If the expression is a constant, return that name. Otherwise return `Name.anonymous`. -/
def constName (e : Expr) : Name :=
e.constName?.getD Name.anonymous
def bvarIdx? : Expr → Option Nat
| bvar idx => some idx
| _ => none
/-- Return the function (name) and arguments of an application. -/
def getAppFnArgs (e : Expr) : Name × Array Expr :=
withApp e λ e a => (e.constName, a)
/-- Turn an expression that is a natural number literal into a natural number. -/
def natLit! : Expr → Nat
| lit (Literal.natVal v) => v
| _ => panic! "nat literal expected"
/-- If an `Expr` has form `.fvar n`, then returns `some n`, otherwise `none`. -/
def fvarId? : Expr → Option FVarId
| .fvar n => n
| _ => none
/-- `isConstantApplication e` checks whether `e` is syntactically an application of the form
`(fun x₁ ⋯ xₙ => H) y₁ ⋯ yₙ` where `H` does not contain the variable `xₙ`. In other words,
it does a syntactic check that the expression does not depend on `yₙ`. -/
def isConstantApplication (e : Expr) :=
e.isApp && aux e.getAppNumArgs'.pred e.getAppFn' e.getAppNumArgs'
where
/-- `aux depth e n` checks whether the body of the `n`-th lambda of `e` has loose bvar
`depth - 1`. -/
aux (depth : Nat) : Expr → Nat → Bool
| .lam _ _ b _, n + 1 => aux depth b n
| e, 0 => !e.hasLooseBVar (depth - 1)
| _, _ => false
open Meta
/-- Check that an expression contains no metavariables (after instantiation). -/
-- There is a `TacticM` level version of this, but it's useful to have in `MetaM`.
def ensureHasNoMVars (e : Expr) : MetaM Unit := do
let e ← instantiateMVars e
if e.hasExprMVar then
throwError "tactic failed, resulting expression contains metavariables{indentExpr e}"
/-- Construct the term of type `α` for a given natural number
(doing typeclass search for the `OfNat` instance required). -/
def ofNat (α : Expr) (n : Nat) : MetaM Expr := do
mkAppOptM ``OfNat.ofNat #[α, mkRawNatLit n, none]
/-- Construct the term of type `α` for a given integer
(doing typeclass search for the `OfNat` and `Neg` instances required). -/
def ofInt (α : Expr) : Int → MetaM Expr
| Int.ofNat n => Expr.ofNat α n
| Int.negSucc n => do mkAppM ``Neg.neg #[← Expr.ofNat α (n+1)]
/--
Return `some n` if `e` is one of the following
- A nat literal (numeral)
- `Nat.zero`
- `Nat.succ x` where `isNumeral x`
- `OfNat.ofNat _ x _` where `isNumeral x` -/
partial def numeral? (e : Expr) : Option Nat :=
if let some n := e.natLit? then n
else
let f := e.getAppFn
if !f.isConst then none
else
let fName := f.constName!
if fName == ``Nat.succ && e.getAppNumArgs == 1 then (numeral? e.appArg!).map Nat.succ
else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then numeral? (e.getArg! 1)
else if fName == ``Nat.zero && e.getAppNumArgs == 0 then some 0
else none
/-- Test if an expression is either `Nat.zero`, or `OfNat.ofNat 0`. -/
def zero? (e : Expr) : Bool :=
match e.numeral? with
| some 0 => true
| _ => false
-- Edit
variable {M}
def modifyAppArgM [Functor M] [Pure M] (modifier : Expr → M Expr) : Expr → M Expr
| app f a => mkApp f <$> modifier a
| e => pure e
def modifyAppArg (modifier : Expr → Expr) : Expr → Expr :=
modifyAppArgM (M := Id) modifier
def modifyRevArg (modifier : Expr → Expr): Nat → Expr → Expr
| 0 => modifyAppArg modifier
| (i+1) => modifyAppArg (modifyRevArg modifier i)
/-- Given `f a₀ a₁ ... aₙ₋₁`, runs `modifier` on the `i`th argument or
returns the original expression if out of bounds. -/
def modifyArg (modifier : Expr → Expr) (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
modifyRevArg modifier (n - i - 1) e
def getRevArg? : Expr → Nat → Option Expr
| app _ a, 0 => a
| app f _, i+1 => getRevArg! f i
| _, _ => none
/-- Given `f a₀ a₁ ... aₙ₋₁`, returns the `i`th argument or none if out of bounds. -/
def getArg? (e : Expr) (i : Nat) (n := e.getAppNumArgs): Option Expr :=
getRevArg? e (n - i - 1)
/-- Given `f a₀ a₁ ... aₙ₋₁`, runs `modifier` on the `i`th argument.
An argument `n` may be provided which says how many arguments we are expecting `e` to have. -/
def modifyArgM [Monad M] (modifier : Expr → M Expr) (e : Expr) (i : Nat) (n := e.getAppNumArgs) :
M Expr := do
let some a := getArg? e i | return e
let a ← modifier a
return modifyArg (fun _ ↦ a) e i n
/-- Traverses an expression `e` and renames bound variables named `old` to `new`. -/
def renameBVar (e : Expr) (old new : Name) : Expr :=
match e with
| app fn arg => app (fn.renameBVar old new) (arg.renameBVar old new)
| lam n ty bd bi =>
lam (if n == old then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi
| forallE n ty bd bi =>
forallE (if n == old then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi
| e => e
open Lean.Meta in
/-- `getBinderName e` returns `some n` if `e` is an expression of the form `∀ n, ...`
and `none` otherwise. -/
def getBinderName (e : Expr) : MetaM (Option Name) := do
match ← withReducible (whnf e) with
| .forallE (binderName := n) .. | .lam (binderName := n) .. => pure (some n)
| _ => pure none
open Lean.Elab.Term
/-- Annotates a `binderIdent` with the binder information from an `fvar`. -/
def addLocalVarInfoForBinderIdent (fvar : Expr) : TSyntax ``binderIdent → TermElabM Unit
| `(binderIdent| $n:ident) => Elab.Term.addLocalVarInfo n fvar
| tk => Elab.Term.addLocalVarInfo (Unhygienic.run `(_%$tk)) fvar
/-- If `e` has a structure as type with field `fieldName`, `mkDirectProjection e fieldName` creates
the projection expression `e.fieldName` -/
def mkDirectProjection (e : Expr) (fieldName : Name) : MetaM Expr := do
let type ← whnf (← inferType e)
let .const structName us := type.getAppFn | throwError "{e} doesn't have a structure as type"
let some projName := getProjFnForField? (← getEnv) structName fieldName |
throwError "{structName} doesn't have field {fieldName}"
return mkAppN (.const projName us) (type.getAppArgs.push e)
/-- If `e` has a structure as type with field `fieldName` (either directly or in a parent
structure), `mkProjection e fieldName` creates the projection expression `e.fieldName` -/
def mkProjection (e : Expr) (fieldName : Name) : MetaM Expr := do
let .const structName _ := (← whnf (←inferType e)).getAppFn |
throwError "{e} doesn't have a structure as type"
let some baseStruct := findField? (← getEnv) structName fieldName |
throwError "No parent of {structName} has field {fieldName}"
let mut e := e
for projName in (getPathToBaseStructure? (← getEnv) baseStruct structName).get! do
let type ← whnf (← inferType e)
let .const _structName us := type.getAppFn | throwError "{e} doesn't have a structure as type"
e := mkAppN (.const projName us) (type.getAppArgs.push e)
mkDirectProjection e fieldName
end Expr
/-- Get the projections that are projections to parent structures. Similar to `getParentStructures`,
except that this returns the (last component of the) projection names instead of the parent names.
-/
def getFieldsToParents (env : Environment) (structName : Name) : Array Name :=
getStructureFields env structName |>.filter fun fieldName =>
isSubobjectField? env structName fieldName |>.isSome
end Lean

27
NNG/Tactic/LeftRight.lean Normal file
View File

@@ -0,0 +1,27 @@
/- Copied from mathlb. -/
import Lean
namespace NNG.Tactic.LeftRight
open Lean Meta Elab Tactic
def leftRightMeta (name : Name) (idx max : Nat) (goal : MVarId) : MetaM (List MVarId) := do
goal.withContext do
goal.checkNotAssigned name
let target ← goal.getType'
matchConstInduct target.getAppFn
(fun _ ↦ throwTacticEx `constructor goal "target is not an inductive datatype")
fun ival us ↦ do
unless ival.ctors.length == max do
throwTacticEx `constructor goal
s!"{name} target applies for inductive types with exactly two constructors"
let ctor := ival.ctors[idx]!
goal.apply <| mkConst ctor us
end LeftRight
open LeftRight
elab "left" : tactic => do
Lean.Elab.Tactic.liftMetaTactic (leftRightMeta `left 0 2)
elab "right" : tactic => do
Lean.Elab.Tactic.liftMetaTactic (leftRightMeta `right 1 2)

2
NNG/Tactic/Rfl.lean
View File

@@ -1,4 +1,4 @@
import Mathlib.Lean.Expr.Basic
import NNG.Tactic.LeanExprBasic
import Lean.Elab.Tactic.Basic
/-! # `rfl` tactic

2
NNG/Tactic/Rw.lean
View File

@@ -1,4 +1,4 @@
import Mathlib.Lean.Expr.Basic
import NNG.Tactic.LeanExprBasic
import Lean.Elab.Tactic.Basic
/-!

4
NNG/Tactic/Simp.lean
View File

@@ -1,4 +1,4 @@
import Mathlib.Lean.Expr.Basic
import NNG.Tactic.LeanExprBasic
import Lean.Elab.Tactic.Basic
import NNG.Tactic.Rfl
@@ -47,5 +47,3 @@ syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
traceSimpCall stx usedSimps
end MyNat

22
lake-manifest.json
View File

@@ -2,27 +2,9 @@
"packagesDir": "lake-packages",
"packages":
[{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
"rev": "fc4a489c2af75f687338fe85c8901335360f8541",
"name": "mathlib",
"inputRev?": "fc4a489c2af75f687338fe85c8901335360f8541"}},
{"git":
{"url": "https://github.com/gebner/quote4",
"subDir?": null,
"rev": "cc915afc9526e904a7b61f660d330170f9d60dd7",
"name": "Qq",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/JLimperg/aesop",
"subDir?": null,
"rev": "071464ac36e339afb7a87640aa1f8121f707a59a",
"name": "aesop",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/leanprover-community/lean4game.git",
"subDir?": "server",
"rev": "b703752f3af7fc895684b687d739f873144f489d",
"rev": "ab0cb5ba3da812762a40fb2f0193d131cf0dad55",
"name": "GameServer",
"inputRev?": "main"}},
{"git":
@@ -30,4 +12,4 @@
"subDir?": null,
"rev": "44a92d84c31a88b9af9329a441890ad449d8cd5f",
"name": "std",
"inputRev?": "main"}}]}
"inputRev?": "44a92d84c31a88b9af9329a441890ad449d8cd5f"}}]}

5
lakefile.lean
View File

@@ -19,9 +19,8 @@ open Lean in
modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName)
: Elab.Command.CommandElabM Unit)
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "fc4a489c2af75f687338fe85c8901335360f8541"
require std from git
"https://github.com/leanprover/std4" @ "44a92d84c31a88b9af9329a441890ad449d8cd5f"
package NNG where
moreLeanArgs := #["-DautoImplicit=false", "-Dtactic.hygienic=false"]