End of namespace

Stream: new members

[Ashvni Narayanan]

I am trying to end a namespace

import ring_theory.ideals

import ring_theory.principal_ideal_domain

universe u

class discrete_valuation_ring (R : Type u) extends principal_ideal_domain R :=

(prime_ideal' : ideal R)

(primality : prime_ideal'.is_prime)

(is_nonzero : prime_ideal' ≠ ⊥)

(unique_nonzero_prime_ideal : ∀ P : ideal R, P.is_prime → P = ⊥ ∨ P = prime_ideal')

namespace discrete_valuation_ring
/- blah blah -/
end dicrete_valuation_ring

I get the errors

command does not accept doc string

and

invalid end of module, expecting 'end'

Any help is appreciated. Thanks!

[Kevin Buzzard]

You have misspelt discrete_valuation_ring in the end version

[Kevin Buzzard]

A docstring is something which looks like /-- blah -/ and it is only allowed to appear directly before a definition or theorem. You can't put it in front of any other command.

[Ashvni Narayanan]

Kevin Buzzard said:

You have misspelt discrete_valuation_ring in the end version

Ah, that is a mistake I made while typing it out. The spelling is correct in the document.

[Kevin Buzzard]

The error command does not accept doc string means that you put a docstring directly above a command.

[Kevin Buzzard]

The error invalid end of module, expecting 'end' means that you opened a section or a namespace with the section or namespace command, and did not close it.

[Kevin Buzzard]

As a general rule, try and fix the first error in your file; other errors might be a weird consequence of Lean getting confused after the first error.

[Ashvni Narayanan]

Ah I got it! Thank you!