safe/unsafe constants

Stream: lean4

[Arthur Paulino]

In Declaration.lean we have:

def isUnsafe : ConstantInfo → Bool
  | defnInfo   v => v.safety == DefinitionSafety.unsafe
  | axiomInfo  v => v.isUnsafe
  | thmInfo    v => false
  | opaqueInfo v => v.isUnsafe
  | quotInfo   v => false
  | inductInfo v => v.isUnsafe
  | ctorInfo   v => v.isUnsafe
  | recInfo    v => v.isUnsafe

What's the meaning of this? What are the causes and consequences of a declaration being unsafe?

[Mac]

Just to clarify, are you simply asking what the unsafe keyword is used for?

[Arthur Paulino]

No, I am asking what it means when a declaration constant returns true on the function above

[Henrik Böving]

I think that is just equivalent to when the unsafe keyword is used on it, at least this is the way doc-gen renders unsafe declarations and it seems to work quite well.