Typoed things are not throwing errors

Stream: lean4

[Bolton Bailey]

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]

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]

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]

@Ruben Van de Velde , you were the person who gave me that settings snippet, is this the same issue?

[Ruben Van de Velde]

If I was, I probably just copied it from mathlib - you could look there

[James Gallicchio]

i don't think it will, but does lake build report it as an error?

[Eric Wieser]

You need to pass moreServerArgs into various places in your lakefile too

[Eric Wieser]

By itself, that code snippet does nothing