Skip to content
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

expr.pis produces a type incorrect expr out of a type correct one #1921

Open
1 task done
cipher1024 opened this issue Feb 4, 2018 · 1 comment
Open
1 task done

Comments

@cipher1024
Copy link
Contributor

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Checked that your issue isn't already filed.
    • Reduced the issue to a self-contained, reproducible test case.

Description

Using expr.pis on a very simple expression resulted in the following error (which I think means some of the intermediate representation for the parser are not removed).

1731:3: unknown declaration '2'
state:
x y : ℕ
⊢ false

Steps to Reproduce

Put the following in a Lean file:

open tactic
example {x y : ℕ}
: false :=
begin
  (do x ← get_local `x,
      p ← to_expr ```(x ≤ y),
      type_check (p.pis [x]),
      trace "success")
end

Expected behavior: [What you expect to happen]

"success" should get printed.

Actual behavior: [What actually happens]

Error:

1731:3: unknown declaration '2'
state:
x y : ℕ
⊢ false

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Lean (version 3.3.1, commit 316d67c3be31, RELEASE)

Mac OS X v 10.13.2

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

@Kha
Copy link
Member

Kha commented Feb 5, 2018

This is not a bug but a feature request for a missing set of APIs that can work with these "special" local constants (called local_decl_refs in the C++ code) derived from a local context in contrast to "regular" locals constructed manually. For reference, here is a simple implementation of pis for this local kind:

namespace tactic
open expr
meta def pis : list expr → expr → tactic expr
| (l::ls) e :=
do local_const uniq pp info _ ← pure l,
   t ← infer_type l,
   e ← pis ls e,
   pure $ pi pp info t (abstract_local e uniq)
| [] e := pure e
end tactic

While this function works with regular locals just as well currently, it is not clear if this is desirable: https://github.com/leanprover/lean/blob/e6a98ffe9c437c157e8b5acb2b9f1e79de66ff1a/src/library/type_context.cpp#L1191. It's probably better to clearly separate these two local kinds.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants