Zulip Chat Archive

Stream: lean4

Topic: Unknown constant ...._spec_N


cognivore (Sep 08 2022 at 16:27):

@Matej Penciak has reduced a fail case I discovered:

import Lean.Data.Parsec

open Lean

variable {α β : Type} {φ : Type  Type} [Monad φ] [Alternative φ]

mutual
  partial def mut1 [Inhabited (φ $ List α)] (p : φ α) (sep : φ β) : φ (List α) :=
    (sep *> mut2 p sep)
  partial def mut2 [Inhabited (φ $ List α)] (p : φ α) (sep : φ β) : φ (List α) :=
    mut1 p sep <|> pure []
end

partial def problem : Parsec Nat := do -- (kernel) unknown constant 'mut2._at.problem._spec_1'
  let asdf  mut2 (pure 1) (pure 2)
  pure 3

It seems like a Lean 4 bug, but I don't understand what does it mean.

Please suggest a way to proceed.

Leonardo de Moura (Sep 08 2022 at 17:55):

This is a bug in the code generator. Could you please create an issue on GitHub?

cognivore (Sep 08 2022 at 18:40):

https://github.com/leanprover/lean4/issues/1573 I hope this will work.


Last updated: Dec 20 2023 at 11:08 UTC