Zulip Chat Archive
Stream: lean4
Topic: difficulty adding string field to type class
David Stainton 🦡 (Aug 28 2024 at 11:51):
Hi. I'm relatively new to Lean. Trying to add a string field called "name" to my NIKE type class:
class Key (key : Type) where
encode : key → ByteArray
decode : ByteArray → Option key
class PrivateKey (privkey : Type) extends Key privkey
class PublicKey (pubkey : Type) extends Key pubkey
class NIKE (scheme : Type) where
PublicKeyType : Type
PrivateKeyType : Type
name : string
privateKeySize : Nat
publicKeySize : Nat
generatePrivateKey : IO PrivateKeyType
derivePublicKey : PrivateKeyType → PublicKeyType
generateKeyPair : IO (PublicKeyType × PrivateKeyType)
groupAction : PrivateKeyType → PublicKeyType → PublicKeyType
encodePrivateKey : PrivateKeyType → ByteArray
decodePrivateKey : ByteArray → Option PrivateKeyType
encodePublicKey : PublicKeyType → ByteArray
decodePublicKey : ByteArray → Option PublicKeyType
For some reason the compiler inference for the name field is:
name : {string : Sort u_1} → string
And I fail to add "name" to existing NIKE class instances:
structure X25519Scheme
instance : nike.NIKE X25519Scheme where
PublicKeyType := PublicKey
PrivateKeyType := PrivateKey
name : String := "X25519"
generatePrivateKey : IO PrivateKey := do
generatePrivateKey
generateKeyPair : IO (PublicKey × PrivateKey) := do
let privKey ← generatePrivateKey
let pubKey := derivePublicKey privKey
pure (pubKey, privKey)
derivePublicKey (sk : PrivateKey) : PublicKey := derivePublicKey sk
groupAction (sk : PrivateKey) (pk : PublicKey) : PublicKey := PublicKey.mk $ curve25519 sk.data pk.data
privateKeySize : Nat := keySize
publicKeySize : Nat := keySize
encodePrivateKey : PrivateKey → ByteArray := fun (sk : PrivateKey) => nike.Key.encode sk
decodePrivateKey : ByteArray → Option PrivateKey := fun (bytes : ByteArray) => nike.Key.decode bytes
encodePublicKey : PublicKey → ByteArray := fun (pk : PublicKey) => nike.Key.encode pk
decodePublicKey : ByteArray → Option PublicKey := fun (bytes : ByteArray) => nike.Key.decode bytes
end CryptWalker.nike.x25519
fails to compile, with:
type mismatch
"X25519"
has type
String : Type
but is expected to have type
{string : Sort ?u.8047} → string : Sort (imax (?u.8047 + 1) ?u.8047)
Edward van de Meent (Aug 28 2024 at 11:53):
string
here is an identifier, while String
is the type of strings... note the capital for the built-in type.
Edward van de Meent (Aug 28 2024 at 11:55):
the reason it doesn't throw an error due to not knowing what string
means here is an option called autoImplicit
, which while true adds unknown identifiers to the context as assumptions.
David Stainton 🦡 (Aug 28 2024 at 11:55):
ah yeah thanks!
Edward van de Meent (Aug 28 2024 at 11:55):
you can turn this off with set_option autoImplicit false
David Stainton 🦡 (Aug 28 2024 at 11:55):
Edward van de Meent said:
you can turn this off with
set_option autoImplicit false
can i set that in my lakefile or does it have to be in the source code of my library?
Edward van de Meent (Aug 28 2024 at 11:57):
i think there is a way to do this in your lakefile, but i don't know it... maybe someone else could help there?
David Stainton 🦡 (Aug 28 2024 at 11:58):
thanks for your help! the error messages were very confusing but i see what i did wrong now at least.
Edward van de Meent (Aug 28 2024 at 12:04):
i don't know if this translates one-to-one, but you could take inspiration from mathlib
s lakefile: https://github.com/leanprover-community/mathlib4/blob/33d4a4af3e67a4561bbb0dacdc9800fc8785fa44/lakefile.lean#L39C1-L53C25
Patrick Massot (Aug 28 2024 at 12:15):
A simpler example can be found at https://github.com/avigad/mathematics_in_lean_source/blob/master/lakefile.lean
David Stainton 🦡 (Aug 28 2024 at 12:16):
Thanks!
Last updated: May 02 2025 at 03:31 UTC