Zulip Chat Archive
Stream: lean4
Topic: (kernel) unknown constant
Sébastien Michelland (May 24 2022 at 14:09):
I have this error, which looks like a Lean bug. It seems that the double-nested dependency is required, the class parameter (specifically a class) is required as well, and the mutual recursion in the string functions is also needed.
class Class where
instance empty: Class := {}
mutual
inductive T (δ: Class) where
| mk (ss: List (S δ))
inductive S (δ: Class) where
| mk (ts: List (T δ))
end
mutual
partial def str_T: T δ → String
| .mk ss => "\n".intercalate (ss.map str_S)
partial def str_S: S δ → String
| .mk ts => "\n".intercalate (ts.map str_T)
end
def error := str_T (T.mk (δ := empty) [])
-- (kernel) unknown constant 'str_T._at.error._spec_1'
Cc @Siddharth Bhat
Sébastien Michelland (May 24 2022 at 16:12):
Temporary workaround for us: make the str_*
functions total by not using map
.
Leonardo de Moura (May 26 2022 at 03:39):
Pushed a fix for this.
Last updated: Dec 20 2023 at 11:08 UTC