lean

Вопрос или проблема import Lean1.Basic structure ArrayN (n : Nat) (α : Type) where array : { array : Array α // array.size = n } class Hash (HashType: Type) where hashSize: Nat hash: x -> ArrayN (hashSize) UInt8 structure Private (Key: Type) (HashType