e181c1adee
The idea is to make clear that the field `posponed` is transient state. It is only used during `isDefEq`. The refactoring was motivated by a bug I found where the `posponed` constraints were not being handled correctly. For example, the `check (e : Expr)` method was returning `true`, but leaving pending universe constraints at `postponed`. cc @Kha
46 lines
1.6 KiB
Text
46 lines
1.6 KiB
Text
doSeqRightIssue.lean:5:24: error: unknown universe level v
|
||
doSeqRightIssue.lean:5:24: error: unknown universe level v
|
||
doSeqRightIssue.lean:7:0: error: don't know how to synthesize placeholder
|
||
context:
|
||
α : Type u
|
||
β : α → (sorryAx (Sort u_1))
|
||
ex : ∀ {p₁p₂ : (sorryAx (Sort u_2))} (h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)), (sorryAx (?m.367 h₁))≅_ → p₁=p₂
|
||
p₁ p₂ : (sorryAx (Sort u_2))
|
||
h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)
|
||
h : (sorryAx (?m.367 _))≅_
|
||
_a_1 _a_2 : (sorryAx (Sort u_2))
|
||
_a_3 : (sorryAx ?m.366)=(sorryAx ?m.366)
|
||
⊢ Prop
|
||
doSeqRightIssue.lean:7:0: error: don't know how to synthesize placeholder
|
||
context:
|
||
α : Type u
|
||
β : α → (sorryAx (Sort u_1))
|
||
ex : ∀ {p₁p₂ : (sorryAx (Sort u_2))} (h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)), (sorryAx (?m.367 h₁))≅_ → p₁=p₂
|
||
p₁ p₂ : (sorryAx (Sort u_2))
|
||
h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)
|
||
h : (sorryAx (?m.367 _))≅_
|
||
_a_1 _a_2 : (sorryAx (Sort u_2))
|
||
⊢ Prop
|
||
doSeqRightIssue.lean:7:66: error: don't know how to synthesize placeholder
|
||
@HEq ?m.367 … … …
|
||
context:
|
||
α : Type u
|
||
β : α → (sorryAx (Sort u_1))
|
||
p₁ p₂ : (sorryAx (Sort u_2))
|
||
h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)
|
||
⊢ Prop
|
||
doSeqRightIssue.lean:7:66: error: don't know how to synthesize placeholder
|
||
@HEq ?m.367 … … …
|
||
context:
|
||
α : Type u
|
||
β : α → (sorryAx (Sort u_1))
|
||
p₁ p₂ : (sorryAx (Sort u_2))
|
||
h₁ : (sorryAx ?m.366)=(sorryAx ?m.366)
|
||
⊢ Prop
|
||
doSeqRightIssue.lean:7:48: error: don't know how to synthesize placeholder
|
||
@Eq ?m.366 … …
|
||
context:
|
||
α : Type u
|
||
β : α → (sorryAx (Sort u_1))
|
||
p₁ p₂ : (sorryAx (Sort u_2))
|
||
⊢ Sort u_3
|