# Zulip Chat Archive

## Stream: new members

### Topic: 2006 STEP 3 Question 8

#### Shing Tak Lam (Mar 23 2020 at 02:53):

Hello, I was trying to formalise my solution to this question in lean, but I'm getting an error saying the my result contains meta variables.

So far I have

import data.polynomial data.real.basic open polynomial variable Δ : polynomial ℝ → polynomial ℝ variables f g : polynomial ℝ variable k : ℝ axiom Δ1 : Δ X = C 1 axiom Δ2 : Δ(f + g) = Δ f + Δ g axiom Δ3 : Δ(C k * f) = C k * Δ f axiom Δ4 : Δ(f * g) = f * Δ g + g * Δ f lemma ΔXcubed : Δ (X^3) = 3*X^2 := begin have h1 : X^3 = X * X^2 := begin have h11 : 3 = 2 + 1 := rfl, rw h11, rw pow_succ, end -- Error Here end

I've highlighted where the error is occuring, the error message is

tactic failed, result contains meta-variables state: no goals state: 6 goals Δ : polynomial ℝ → polynomial ℝ ⊢ Δ (X ^ 3) = 3 * X ^ 2 Δ : polynomial ℝ → polynomial ℝ ⊢ Type ? Δ : polynomial ℝ → polynomial ℝ ⊢ comm_semiring ?m_1 Δ : polynomial ℝ → polynomial ℝ ⊢ has_pow (polynomial ?m_1) ℕ Δ : polynomial ℝ → polynomial ℝ ⊢ has_mul (polynomial ?m_1) Δ : polynomial ℝ → polynomial ℝ ⊢ has_pow (polynomial ?m_1) ℕ

I think I know why the error is occurring, as I didn't specify the type of X, so lean doesn't know that it has `pow`

`mul`

, etc. But I'm not sure how or where I could add the type annotations?

Also, when I use the axioms, `rw \Delta4`

doesn't work, I need to specify `rw \Delta4 \Delta`

. Making `\Delta`

a `constant`

fixes this, but then it still doesn't fix the error message above. In this case, should `\Delta`

be `variable`

or `constant`

? Since I don't care what `Delta`

is, as long as it satisfies those axioms.

#### Mario Carneiro (Mar 23 2020 at 02:59):

those `axiom`

s should be `variable`

s. If you make them `axiom`

s then they will implicitly quantify over all Delta, meaning that you are adding an axiom to lean that says that all functions are derivations. Since this is false, the axiom will make lean inconsistent

#### Yury G. Kudryashov (Mar 23 2020 at 03:01):

And you probably want to `include`

all these variables so that they will be available in tactic proofs.

#### Shing Tak Lam (Mar 23 2020 at 03:30):

Alright thank you, I've edited it with your suggestions. However, I still have an issue with the `results contains meta-variables`

.

#### Yury G. Kudryashov (Mar 23 2020 at 03:33):

Can't help without looking at your code...

#### Shing Tak Lam (Mar 23 2020 at 03:36):

Apologies. The error message is basically the same after changing the `axioms`

to `variables`

. I've also changed `f`

`g`

and `k`

to be in `forall`

s instead of `variables`

.

import data.polynomial data.real.basic open polynomial variable Δ : polynomial ℝ → polynomial ℝ include Δ variable Δ1 : Δ X = C 1 variable Δ2 : ∀ (f g : polynomial ℝ), Δ(f + g) = Δ f + Δ g variable Δ3 : ∀ (k : ℝ) (f : polynomial ℝ), Δ(C k * f) = C k * Δ f variable Δ4 : ∀ (f g : polynomial ℝ), Δ(f * g) = f * Δ g + g * Δ f include Δ1 Δ2 Δ3 Δ4 lemma ΔXcubed : Δ (X^3) = 3*X^2 := begin have h1 : X^3 = X * X^2 := begin have h11 : 3 = 2 + 1 := rfl, rw h11, rw pow_succ, end -- ERROR HERE end

#### Shing Tak Lam (Mar 23 2020 at 03:38):

Nevermind, I've figured it out. I needed to add the type annotation in the inner `have`

statement, as the `X`

in the inner statement is different to the one in the theorem statement.

#### Mario Carneiro (Mar 23 2020 at 03:41):

you can prove `h1`

`by ring`

#### Shing Tak Lam (Mar 23 2020 at 03:49):

Alright, Thanks!

#### Kevin Buzzard (Mar 23 2020 at 07:07):

Did you try `recover`

?

This is a great question for Lean!

#### Kevin Buzzard (Mar 23 2020 at 07:45):

I think you might be better off proving `lemma Δ_one : Δ 1 = 0`

first, and then `lemma ΔX_pow_succ (n : ℕ) : Δ (X ^ (n + 1)) = (n + 1) * X ^ n`

#### Shing Tak Lam (Mar 23 2020 at 07:47):

I'm sorry, but I'm not sure what you mean by using `recover`

.

#### Shing Tak Lam (Mar 23 2020 at 07:47):

I've already proved that `\Delta c = 0`

for all `c`

.

#### Shing Tak Lam (Mar 23 2020 at 07:47):

I've already proved that `\Delta c = 0`

for all `c`

.

#### Shing Tak Lam (Mar 23 2020 at 07:47):

I'm sorry, but I'm not sure what you mean by using `recover`

.

#### Shing Tak Lam (Mar 23 2020 at 07:48):

And I did prove the general case of `X^n`

, although I used `X^n`

and not `X^(n+1)`

, which had an interesting base case

#### Kevin Buzzard (Mar 23 2020 at 07:48):

Oh, `recover`

was when your goal contained metavariables.

#### Shing Tak Lam (Mar 23 2020 at 07:48):

Ah. I see

#### Kevin Buzzard (Mar 23 2020 at 07:49):

The problem with `X^n`

directly is that when n=1 the inductive hypothesis involves 0 - 1 so has to be dealt with as a special case.

#### Shing Tak Lam (Mar 23 2020 at 07:50):

Yeah, when I was doing this question for STEP prep I thought it would be interesting to do in lean, as the steps revolved around these 4 rules. Now that no one even knows what's gonna happen with A Levels/STEP I had a bit of free time so I thought I'd give it a shot in Lean.

#### Kevin Buzzard (Mar 23 2020 at 07:51):

My son is in the same position -- sitting on a Cambridge offer with no idea what's going to happen next.

#### Shing Tak Lam (Mar 23 2020 at 07:51):

That makes sense, I did it on paper first and tried a direct translation. In retrospect `X^(n+1)`

makes more sense. I'm gonna refactor it.

#### Shing Tak Lam (Mar 23 2020 at 07:52):

Yeah, Cambridge sent out an email like hours before the Government announcement, which wasn't that helpful.

(Not that any of my other Universities seem to know what is happening, do you know anything about Imperial?)

#### Kevin Buzzard (Mar 23 2020 at 07:52):

No decisions have been made yet.

#### Shing Tak Lam (Mar 23 2020 at 07:53):

Alright. Just that they haven't said anything since January, which was slightly worrying.

#### Shing Tak Lam (Mar 23 2020 at 07:53):

Thank you very much for all of your help

#### Kevin Buzzard (Mar 23 2020 at 08:17):

lemma Δ_one : Δ 1 = 0 := begin -- the standard trick suffices H : Δ 1 + Δ 1 = Δ 1, rwa add_left_eq_self at H, conv begin to_rhs, rw (show (1 : polynomial ℝ) = 1 * 1, by ring), end, rw Δ4, ring, end lemma ΔX_pow_succ (n : ℕ) : Δ (X ^ (n + 1)) = (n + 1) * X ^ n := begin induction n with d hd, { -- base case rw [pow_one, Δ1, nat.cast_zero], ring, }, rw [nat.succ_eq_add_one, pow_succ, Δ4, Δ1, hd, pow_succ, nat.cast_add, nat.cast_one], ring, end

#### Kevin Buzzard (Mar 23 2020 at 08:22):

It helps a lot knowing what `ring`

can and cannot do.

#### Shing Tak Lam (Mar 23 2020 at 08:31):

Again, thank you very much.

This (once again) reminds me I should probably read TPIL. `show`

is nicer than what I've been doing, which is `have`

then `rw`

, which clutters up my local context a lot, and I end up with a lot of local hypotheses which are only used once.

For the final part of the question, the proof that `\Delta f = df/dx`

for all polynomial `f`

, I did it (on paper) by arguing that it's true for a polynomial of degree 1 (and 0), and then using induction, assuming that it is true for a polynomial of degree `n`

then showing that it's true for a polynomial of degree `n+1`

, therefore it is true for all polynomials. I've tried looking in `data.polynomial`

, but I don't think I've seen this functionality in there. So I might have to do it another way.

I'm gonna look `ring`

(and probably what a ring is first).

#### Mario Carneiro (Mar 23 2020 at 08:54):

This is just induction on natural numbers

#### Mario Carneiro (Mar 23 2020 at 08:55):

I'm pretty sure there is a `degree`

function on polynomials

#### Mario Carneiro (Mar 23 2020 at 08:56):

The question I have about this problem is, do we have the definition of the derivative of a polynomial yet? Do we know it is a polynomial? I'm not sure how you intend to write the theorem statement

#### Johan Commelin (Mar 23 2020 at 08:58):

Mario Carneiro said:

I'm pretty sure there is a

`degree`

function on polynomials

Yes, and there is also `nat_degree`

which is a natural number. (`degree 0`

is not natural)

#### Shing Tak Lam (Mar 23 2020 at 08:59):

So induction on `degree p`

where `p`

is the polynomial? The `degree`

function returns an `option nat`

though, so I'll have to look at that further.

I haven't written it yet, but there is a `polynomial.derivative`

function, so I think it'll just be `forall (p : polynomial R), derivative p = \Delta p`

.

#### Johan Commelin (Mar 23 2020 at 08:59):

We have the formal derivative of a polynomial, and also a proof that as a function it coincides with the analytical derivative (if you work over a normed field or something)

#### Mario Carneiro (Mar 23 2020 at 08:59):

nice

#### Sebastien Gouezel (Mar 23 2020 at 09:26):

There is a function `polynomial.induction_on`

that is designed precisely for this kind of induction. You can for instance have a look at `analysis/calculus/deriv`

, line 1116.

#### Shing Tak Lam (Mar 23 2020 at 09:36):

Ok. Thank you all very much. I'll give that a shot when I have some more time to look at this.

#### Shing Tak Lam (Mar 23 2020 at 11:43):

I've had some free time just then and I tried Kevin's solution from above. However when i pasted it into lean I got a `(deterministic) timeout`

. Seems like the `ring`

s are taking too long. I doubt my laptop is too slow, but that is a possibility.

Any suggestions to how I can fix this?

#### Mario Carneiro (Mar 23 2020 at 11:44):

`ring`

performs very fast on almost all not-contrived examples, so that's not likely to be the problem

#### Mario Carneiro (Mar 23 2020 at 11:44):

it could be typeclass inference or something else

#### Mario Carneiro (Mar 23 2020 at 11:44):

code plz

#### Shing Tak Lam (Mar 23 2020 at 11:47):

Minimum Working Example

import data.polynomial data.real.basic tactic open polynomial variable Δ : polynomial ℝ → polynomial ℝ include Δ variable Δ1 : Δ X = C 1 variable Δ2 : ∀ (f g : polynomial ℝ), Δ(f + g) = Δ f + Δ g variable Δ3 : ∀ (k : ℝ) (f : polynomial ℝ), Δ(C k * f) = C k * Δ f variable Δ4 : ∀ (f g : polynomial ℝ), Δ(f * g) = f * Δ g + g * Δ f include Δ1 Δ2 Δ3 Δ4 lemma ΔXn (n : ℕ) : Δ (X^(n+1)) = (n+1)*X^n := begin induction n with d hd, { -- base case rw [pow_one, Δ1, nat.cast_zero], ring, }, rw [nat.succ_eq_add_one, pow_succ, Δ4, Δ1, hd, pow_succ, nat.cast_add, nat.cast_one], ring, end

The lemma is just the one Kevin posted above, so it probably worked on his machine.

#### Shing Tak Lam (Mar 23 2020 at 11:48):

It might be of use: `#eval lean.version`

is `(3, (6, 1))`

, `mathlib`

is `mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "093ac77ac9d27ce83ebf4e76ca5bd9b3eaebedaa"}`

#### Shing Tak Lam (Mar 23 2020 at 11:49):

The lemma checks almost immediately if I comment out the `ring`

in the inductive case (the one at the end of the lemma)

#### Mario Carneiro (Mar 23 2020 at 11:57):

The goal you gave to `ring`

is

⊢ X * ((↑d + 1) * X ^ d) + X * X ^ d * C 1 = (↑d + 1 + 1) * (X * X ^ d)

which is not an equality that is valid from the axioms of rings alone (because of the `C 1`

)

#### Mario Carneiro (Mar 23 2020 at 11:59):

I think `ring`

is probably taking forever because it does some processing to see if different looking expressions are defeq, and it is unfolding `C 1`

#### Mario Carneiro (Mar 23 2020 at 12:00):

IIRC there is an option to disable that, but then it will just fail in this case

#### Mario Carneiro (Mar 23 2020 at 12:01):

This works

lemma ΔXn (n : ℕ) : Δ (X^(n+1)) = (n+1)*X^n := begin induction n with d hd, { -- base case rw [pow_one, Δ1, nat.cast_zero], ring, }, rw [nat.succ_eq_add_one, pow_succ, Δ4, Δ1, hd, pow_succ, nat.cast_add, nat.cast_one, C_1], ring, end

#### Shing Tak Lam (Mar 23 2020 at 12:01):

Huh... Alright. (I didn't write this).

Adding `rw (show C (1:ℝ) = 1, by simp),`

before `ring`

fixed this.

Thank you very much.

#### Mario Carneiro (Mar 23 2020 at 12:02):

Alternatively you can probably use `simp`

instead of `rw`

since half of those equations are simp lemmas

#### Shing Tak Lam (Mar 23 2020 at 12:03):

I see. I thought I saw somewhere that it's best to only use `simp`

as the last tactic in a proof. That's why I didn't use it there.

#### Johan Commelin (Mar 23 2020 at 12:04):

That's right

#### Johan Commelin (Mar 23 2020 at 12:04):

But `simp only`

is fine

#### Johan Commelin (Mar 23 2020 at 12:04):

Write `squeeze_simp`

to get some help

#### Mario Carneiro (Mar 23 2020 at 12:04):

lemma ΔXn (n : ℕ) : Δ (X^(n+1)) = (n+1)*X^n := begin induction n with d hd, { -- base case rw [pow_one, Δ1, nat.cast_zero], ring, }, rw [pow_succ, Δ4, hd], simp [Δ1, pow_succ], ring, end

#### Mario Carneiro (Mar 23 2020 at 12:05):

using `simp`

before a tactic that doesn't care too much about the shape of the input, like `ring`

, is okay

#### Shing Tak Lam (Mar 23 2020 at 12:06):

Ok. Thank you.

#### Shing Tak Lam (Mar 23 2020 at 12:24):

Another question, when I try to `rw ΔXn`

, it doesn't work. But `rw ΔXn Δ`

works. But then it puts all of `Δ1 Δ2 Δ3 Δ4`

as new goals. Why? It's easy to solve (`repeat {assumption}`

), but I'd still like to know why this is the case.

#### Kevin Buzzard (Mar 23 2020 at 13:16):

Because you used variables

#### Kevin Buzzard (Mar 23 2020 at 13:17):

The theorems you're proving are "if Delta satisfies all these axioms then..." and the proofs are hence all functions which demand proofs of all the axioms as input

#### Kevin Buzzard (Mar 23 2020 at 13:18):

One way around this would probably be to make some sort of structure to carry the variables around in

#### Mario Carneiro (Mar 23 2020 at 13:20):

You can probably also use `parameters`

but it doesn't take much to stumble on places where they don't work very well

#### Kevin Buzzard (Mar 23 2020 at 13:22):

If you used parameters you would probably be able to avoid this issue in this one particular lean file, but if someone were to import your file because they wanted to use your work, the extra assumptions would be back by default

#### Kevin Buzzard (Mar 23 2020 at 13:22):

And the user could probably try to `include`

them but then they have to remember to `exclude`

them later. This set up happens very little in mathlib

#### Mario Carneiro (Mar 23 2020 at 13:23):

I think that's what you want in this case though. There are two or three intermediate lemmas and you don't want to refer to the assumptions since they are fixed, but once you reach the goal, you discharge everything and it becomes a regular theorem with a bunch of hypotheses

#### Kevin Buzzard (Mar 23 2020 at 13:24):

Here's how it would work with structures. You could define delta-structure on a ring R to be a function called Delta from polynomial R to polynomial R which satisfied the axioms. Just like the definition of a group in the group theory game.

#### Mario Carneiro (Mar 23 2020 at 13:25):

I think it has a name, it's called a derivation

#### Kevin Buzzard (Mar 23 2020 at 13:26):

And then you want to prove that if Delta is any delta-structure then the underlying map Delta.to_fun must agree with differentiation

#### Kevin Buzzard (Mar 23 2020 at 13:27):

A general derivation goes from R to another ring A and there is no Delta 1 axiom

#### Kevin Buzzard (Mar 23 2020 at 13:28):

The advantage of the structure approach is that you have easy access to the axioms: Delta.map_add is Delta2 for the function Delta.to_fun for example

#### Kevin Buzzard (Mar 23 2020 at 13:29):

Delta4 will be called Delta.map_mul

#### Kevin Buzzard (Mar 23 2020 at 13:30):

And someone better at knowing Lean's naming convention can figure out what Delta3 is called

#### Mario Carneiro (Mar 23 2020 at 13:30):

something with `smul`

?

#### Kevin Buzzard (Mar 23 2020 at 13:34):

Oh is it not in canonical form??

#### Kevin Buzzard (Mar 23 2020 at 13:35):

I understand this canonical form/naming convention far worse than I would like to

#### Mario Carneiro (Mar 23 2020 at 13:43):

No, I think it's fine to write `C k * p`

instead of `k \bu p`

since it's an algebra

#### Mario Carneiro (Mar 23 2020 at 13:43):

I just meant that something like `map_smul`

could be used for the name

#### Mario Carneiro (Mar 23 2020 at 13:43):

but since it isn't written with `\bu`

that's a bit of a lie, so perhaps `map_C_mul`

is better

#### Kevin Buzzard (Mar 23 2020 at 13:52):

The correct theorem from the point of view of derivations is that if we have a structure satisfying the last three axioms then there exists a unique polynomial g such that Delta (f) = g*f', and that g can be taken to be Delta(X)

#### Kevin Buzzard (Mar 23 2020 at 13:52):

This has the original question as a special case

#### Kevin Buzzard (Mar 23 2020 at 13:54):

Do we have a theory of derivations in Lean already? @Johan Commelin ?

#### Kevin Buzzard (Mar 23 2020 at 13:55):

I think it would be quite fun to prove the universal property of derivations in general.

#### Mario Carneiro (Mar 23 2020 at 13:59):

pretty sure we don't

#### Kevin Buzzard (Mar 23 2020 at 14:02):

@Shing Tak Lam so there's your homework while your teachers go through all the people in your year awarding them A-levels. I wonder if they'll do it anonymously?

#### Kevin Buzzard (Mar 23 2020 at 14:02):

Feel free to ask if you need help

#### Kevin Buzzard (Mar 23 2020 at 14:03):

But let's make a new thread because this one has a silly name. It can go in #maths

#### Shing Tak Lam (Mar 23 2020 at 14:05):

I had a meeting with my teachers earlier, and as I'm doing International A Levels, apparently my exams are still going ahead... It's just STEP that's a maybe...

Apparently the exam boards think that it's safe to go ahead (even though IB has cancelled for everyone as well).

#### Shing Tak Lam (Mar 23 2020 at 14:05):

So I guess I still have to revise...

#### Shing Tak Lam (Mar 23 2020 at 14:06):

(deleted)

#### Johan Commelin (Mar 23 2020 at 14:11):

Kevin Buzzard said:

Do we have a theory of derivations in Lean already? Johan Commelin ?

Not yet, but @Kenny Lau looked into it at some point, I htink.

#### Kenny Lau (Mar 23 2020 at 14:12):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/derivation/near/170730598

#### Kevin Buzzard (Mar 23 2020 at 14:17):

Has enough API been extracted?

#### Johan Commelin (Mar 23 2020 at 14:17):

What are you thinking of?

#### Kevin Buzzard (Mar 23 2020 at 14:18):

Did we locate the characteristic predicate yet?

#### Kevin Buzzard (Mar 23 2020 at 14:18):

I think this has something to do with transfer.

#### Johan Commelin (Mar 23 2020 at 14:19):

No, I don't think much happened so far.

#### Johan Commelin (Mar 23 2020 at 14:19):

Also, didn't we switch to calling it the "characteristic predicate"?

#### Kevin Buzzard (Mar 23 2020 at 14:20):

Somehow the bare minimum API is the universal property, and then there is the problem of isolating the characteristic predicate and proving that a module satisfies the characteristic predicate iff it's the differentials

#### Kevin Buzzard (Mar 24 2020 at 13:47):

@Kenny Lau

import data.polynomial open polynomial structure delta_structure (R : Type) [comm_ring R] := (to_fun : polynomial R → polynomial R) (map_X' : to_fun X = 1) (map_add' : ∀ (f g : polynomial R), to_fun (f + g) = to_fun f + to_fun g) (map_C_mul' : ∀ (k : R) (f : polynomial R), to_fun (C k * f) = C k * to_fun f) (map_mul' : ∀ (f g : polynomial R), to_fun (f * g) = f * to_fun g + g * to_fun f) namespace delta_structure variables {R : Type} [comm_ring R] (Δ : delta_structure R) instance : has_coe_to_fun (delta_structure R) := ⟨_, to_fun⟩ @[simp] theorem map_X (Δ : delta_structure R) : Δ X = 1 := Δ.map_X' @[simp] theorem map_add (Δ : delta_structure R) : ∀ {f g : polynomial R}, Δ (f + g) = Δ f + Δ g := Δ.map_add' @[simp] theorem map_C_mul : ∀ (k : R) (f : polynomial R), Δ (C k * f) = C k * Δ f := Δ.map_C_mul' @[simp] theorem map_mul : ∀ (f g : polynomial R), Δ (f * g) = f * Δ g + g * Δ f := Δ.map_mul' end delta_structure

What do you think of my structure?

#### Kevin Buzzard (Mar 27 2020 at 12:46):

@Shing Tak Lam now has a github repo where this question is solved using derivations on a polynomial ring. @Patrick Massot at the time of writing I see that he only has one branch, which is `lean-3.4.2`

. Is this something to do with the tooling? Shing -- did you use `leanproject`

to make this repo?

#### Kevin Buzzard (Mar 27 2020 at 12:50):

the linter doesn't like the `simp`

s above but now I have a much better understanding of what is going on there.

#### Shing Tak Lam (Mar 27 2020 at 12:58):

Yes I did use `leanproject`

. Just to check I made a new project.

$ leanproject new test > mkdir -p test > cd test > mkdir src > git init -q > git checkout -b lean-3.4.2 Switched to a new branch 'lean-3.4.2' configuring test 0.1 Adding mathlib

I'm kinda confused now as that shouldn't be happening...

Looking at the repo at https://github.com/leanprover-community/mathlib-tools/blob/96734b3f6e7b1b6d69f86e18f4fee9c4c3e8bfff/mathlibtools/lib.py#L435 the branch should be called `master`

.

#### Shing Tak Lam (Mar 27 2020 at 12:59):

For what it's worth

$ pip list | grep mathlibtools mathlibtools 0.0.4

#### Kevin Buzzard (Mar 27 2020 at 12:59):

The tooling is brand new, much better than what we had before, but still contains a few minor glitches. It has already transformed my workflow though.

#### Kevin Buzzard (Mar 27 2020 at 12:59):

Yeah, that number is an indication of how new it is :-)

#### Patrick Massot (Mar 27 2020 at 13:35):

`leanproject`

still uses leanpkg to create new projects. And leanpkg uses the default elan toolchain. We should change that, but that requires finding time to do it.

#### Patrick Massot (Mar 27 2020 at 13:36):

Also note that every complain or feature request about leanproject that is expressed here but not in a GitHub issue currently falls into a black hole.

#### Shing Tak Lam (Mar 27 2020 at 14:22):

Mhm... I found

https://github.com/leanprover-community/mathlib-tools/issues/26

and

So this should be fixed...

#### Patrick Massot (Mar 27 2020 at 14:32):

The lean-3.4.2 exists in your repository, but the master branch also exist. Did you need to manually merge one branch into the other?

#### Shing Tak Lam (Mar 27 2020 at 14:36):

That was me renaming the branch locally from lean-3.4.2 to master then pushing it.

#### Shing Tak Lam (Mar 27 2020 at 14:37):

lean-3.4.2 now only exists on github but not on my local copy. I can probably delete it.

#### Patrick Massot (Mar 27 2020 at 14:50):

I'm sorry I can't reproduce this locally.

$ leanproject new test $ git a leanpkg.toml $ git commit $ git branch * master

#### Shing Tak Lam (Mar 27 2020 at 14:52):

No problem. I have a few ideas on what may have caused this, I'll give it a go tomorrow. If I find anything then I'll report back.

Last updated: May 08 2021 at 18:17 UTC