Zulip Chat Archive

Stream: new members

Topic: unknown identifier linarith and \R


Ayush Agrawal (Oct 01 2021 at 08:41):

Hi Guys! Can someone help me in figuring out why the code is not able to recognize \R and linarith. Is this due to dynamic updates that are happening or am I missing some imports. This was working fine yesterday.
image.png
image.png
Thanks in advance!

Johan Commelin (Oct 01 2021 at 08:43):

@Ayush Agrawal What are the imports at the top of the file?

Ayush Agrawal (Oct 01 2021 at 08:47):

@Johan CommelinHi! I am attaching the file of the imports. import_lib.lean Please advise!

Johan Commelin (Oct 01 2021 at 08:50):

Could you please just copy paste the import statements in a codeblock

```
code goes here
```

Ayush Agrawal (Oct 01 2021 at 08:54):

import algebra.algebra.basic
import algebra.big_operators.basic
import algebra.floor
import algebra.group_power.basic
import algebra.quadratic_discriminant
import algebra.ring.basic
import analysis.asymptotics.asymptotic_equivalent
import analysis.mean_inequalities
import analysis.normed_space.basic
--import analysis.inner_product_space.basic
--import analysis.inner_product_space.euclidean_dist
import analysis.normed_space.pi_Lp
--import analysis.special_functions.exp_log
--import analysis.special_functions.pow
--import analysis.special_functions.trigonometric.basic
import combinatorics.simple_graph.basic
import data.complex.basic
import data.complex.exponential
import data.equiv.basic
import data.finset.basic
import data.int.basic
import data.int.gcd
import data.int.modeq
import data.list.palindrome
import data.multiset.basic
import data.nat.basic
import data.nat.choose.basic
import data.nat.digits
--import data.nat.factorial.basic
import data.nat.modeq
import data.nat.parity
import data.nat.prime
import data.pnat.basic
import data.polynomial
import data.polynomial.basic
import data.polynomial.eval
import data.rat.basic
import data.real.basic
import data.real.ennreal
import data.real.irrational
import data.real.nnreal
import data.real.sqrt
import data.sym.sym2
import data.zmod.basic
import geometry.euclidean.basic
import geometry.euclidean.circumcenter
import geometry.euclidean.monge_point
import geometry.euclidean.sphere
import init.data.nat.gcd
import linear_algebra.affine_space.affine_map
import linear_algebra.affine_space.independent
import linear_algebra.affine_space.ordered
import linear_algebra.finite_dimensional
import measure_theory.integral.interval_integral
import number_theory.arithmetic_function
import order.bounds
import order.filter.basic
--import topology.basic
--import topology.instances.nnreal

Hope its fine now!

Johan Commelin (Oct 01 2021 at 08:54):

Wow! That's a looong list of imports.

Johan Commelin (Oct 01 2021 at 08:55):

You know that imports are transitive? I guess you can remove 80% of them.

Ayush Agrawal (Oct 01 2021 at 08:55):

oh! I didn't know this. Can you shed a bit more light on this?

Ayush Agrawal (Oct 01 2021 at 08:56):

Is this causing problems in running linarith tactic?

Johan Commelin (Oct 01 2021 at 08:56):

If you have import foo.bar.quux and import baz.xyzzy, but baz/xyzzy.lean contains import foo.bar.quux, then you can remove import foo.bar.quux.

Johan Commelin (Oct 01 2021 at 08:57):

I don't think this is causing your problem.

Johan Commelin (Oct 01 2021 at 08:57):

@Ayush Agrawal Is this the first error in your file? Or do you have other errors higher up?

Johan Commelin (Oct 01 2021 at 08:57):

What is the error message on the ?

Ayush Agrawal (Oct 01 2021 at 08:59):

this is the only error in the file rest of the simple tactics like rw, intro etc are working fine. its unknown identifier ℝ
``

Johan Commelin (Oct 01 2021 at 09:01):

Is your repo publically available?

Ayush Agrawal (Oct 01 2021 at 09:02):

No I don't think so.

Ayush Agrawal (Oct 01 2021 at 09:03):

I have just installed Lean on windows and started working on vscode. I have not linked the work to a github repo yet.

Johan Commelin (Oct 01 2021 at 09:06):

Weird. You certainly have the right imports.

Johan Commelin (Oct 01 2021 at 09:07):

If you can push your repo online, it will be easier to debug this.

Ayush Agrawal (Oct 01 2021 at 09:08):

Sure @Johan Commelin will notify you after pushing the repo online

Ayush Agrawal (Oct 01 2021 at 14:52):

@Johan Commelin Now that error is not coming..strange!

Johan Commelin (Oct 01 2021 at 18:05):

@Ayush Agrawal Oh well... I'm glad it's gone (-;


Last updated: Dec 20 2023 at 11:08 UTC