Zulip Chat Archive

Stream: general

Topic: Filling metavariables when given partial information


Tomas Skrivan (Oct 11 2020 at 09:42):

Let's have an expression (λ x : _, x), is there a way to turn it into (λ x : nat, x) if I know its type should be _ → nat?

My attempt:

run_cmd do
  pe  tactic.to_expr  ``(λ x, x) tt ff,
  `(%%e : %%M  nat)  pure pe,
  tactic.trace e

However this still prints λ (x : ?m_1), x. Is there a simple way to achieve this?

Mario Carneiro (Oct 11 2020 at 09:48):

run_cmd do
  let p : pexpr := ``(λ x, x),
  e  tactic.to_expr ``(%%p : _  nat),
  tactic.trace e

Tomas Skrivan (Oct 11 2020 at 10:23):

Thanks, but assuming nat → _ instead of _ → nat fails to infer the type. Why is that?

Tomas Skrivan (Oct 11 2020 at 10:39):

Also I would like to be able to partially infer types. E.g. for expression (λ x y, x) given it has the type _ → _ → natconcluding that it is (λ (x : nat) (y : _), x).

run_cmd do
  let p : pexpr := ``(λ x y, x),
  e  tactic.to_expr ``(%%p : _  _  nat),
  tactic.trace e

Mario Carneiro (Oct 11 2020 at 10:44):

Lean will almost never let you write nat -> _

Mario Carneiro (Oct 11 2020 at 10:45):

because it produces a metavariable that depends on another variable, which doesn't unify with anything

Mario Carneiro (Oct 11 2020 at 10:46):

Note that lean is doing dependent type theory, even if you aren't

Mario Carneiro (Oct 11 2020 at 10:46):

so arrows are hard

Mario Carneiro (Oct 11 2020 at 10:50):

This has a slightly more comprehensible result:

run_cmd do
  let p : pexpr := ``(λ x y, x),
  expr.app (expr.app e _) _  tactic.to_expr ``(%%p _ _ : nat) tt tt,
  tactic.trace e

Mario Carneiro (Oct 11 2020 at 10:50):

and you can also do nat -> _ that way, e.g. using ``(%%p (_ : nat) _)

Tomas Skrivan (Oct 11 2020 at 10:58):

I see that with dependent types it gets really difficult. (You have a slight typo, there should be tactic.to_expr ... tt ff)


Last updated: Dec 20 2023 at 11:08 UTC