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.