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