Zulip Chat Archive
Stream: lean4
Topic: Typoed things are not throwing errors
Bolton Bailey (Sep 10 2023 at 05:30):
I have the following MWnotE
import Mathlib.Algebra.Field.Basic
import Mathlib.Data.MvPolynomial.CommRing
section
structure StraightforwardAGMProofSystem (F : Type) [Field F] (n_stmt n_wit : ℕ) where
relation : (Fin n_stmt → F) → (Fin n_wit → F) → Prop
nSample : ℕ
nCrs : ℕ
crs_elems : Fin n_crs → MvPolynomial (Fin n_sample) F
How do I make this throw an error?
Bolton Bailey (Sep 10 2023 at 05:30):
I thought all I had to do was put
def moreServerArgs := #[
"-Dpp.unicode.fun=true", -- pretty-prints `fun a ↦ b`
"-DAutoImplicit=false"
]
In my lakefile, but that's already there
Bolton Bailey (Sep 10 2023 at 05:39):
To make it clear, I would like this to throw an error because the n_crs
is supposed to be the same as nCrs
.
Bolton Bailey (Sep 10 2023 at 05:41):
@Ruben Van de Velde , you were the person who gave me that settings snippet, is this the same issue?
Ruben Van de Velde (Sep 10 2023 at 06:24):
If I was, I probably just copied it from mathlib - you could look there
James Gallicchio (Sep 10 2023 at 06:31):
i don't think it will, but does lake build
report it as an error?
Eric Wieser (Sep 10 2023 at 08:36):
You need to pass moreServerArgs
into various places in your lakefile too
Eric Wieser (Sep 10 2023 at 08:36):
By itself, that code snippet does nothing
Last updated: Dec 20 2023 at 11:08 UTC