43 lines
1.2 KiB
Text
43 lines
1.2 KiB
Text
axiom Foo : Type
|
||
axiom foo : Foo
|
||
|
||
/- This works -/
|
||
def works : Prop :=
|
||
-- ∀ (x : Foo),
|
||
let ⟨foo₁, foo₂⟩ := (foo, foo);
|
||
false
|
||
|
||
/-
|
||
The following tests fail because the elaborator fails to propagate the expected type. The main issue is that the elaborator is missing the following case:
|
||
|
||
If the expected type is `Prop` for an expression `Forall (x : A), t`, then we should also elaborate `t` with expected type `Prop`. Note that every single example works if we write them as `Forall (x : A), (t : Prop)`.
|
||
-/
|
||
|
||
/- Uncommenting breaks it -/
|
||
def fails₁ : Prop :=
|
||
∀ (x : Foo),
|
||
let ⟨foo₁, foo₂⟩ := (foo, foo);
|
||
false
|
||
-- let_destruct_inside_forall.lean:11:4: error: invalid match/convoy expression, expected type is not known
|
||
|
||
/- All the following variations fail as well with the same message -/
|
||
def fails₂ : Prop :=
|
||
∀ (x : Foo),
|
||
let (⟨foo₁, foo₂⟩ : Foo × Foo) := (foo, foo);
|
||
foo₁ = foo₂
|
||
|
||
def fails₃ : Prop :=
|
||
∀ (x : Foo),
|
||
let (⟨foo₁, foo₂⟩ : Foo × Foo) := (foo, foo);
|
||
false
|
||
|
||
def fails₄ : Prop :=
|
||
∀ (x : Foo),
|
||
let (⟨foo₁, foo₂⟩ : Foo × Foo) := ((foo, foo) : Foo × Foo);
|
||
false
|
||
|
||
def fails₅ : Prop :=
|
||
∀ (x : Foo),
|
||
let p : Foo × Foo := (foo, foo);
|
||
let ⟨foo₁, foo₂⟩ := p;
|
||
foo₁ = foo₂
|