opaque imitDepFn : Lean.Option Bool

def DUnif.withoutModifyingMCtx {α : Type} (x : Lean.MetaM α) : Lean.MetaM α

Equations

• DUnif.withoutModifyingMCtx x = do let s ← Lean.getMCtx tryFinally x (Lean.setMCtx s)

def DUnif.iteration (F : Lean.Expr) (p : UnifProblem) (eq : UnifEq) (funcArgOnly : Bool) : Lean.MetaM (Duper.LazyList (Lean.MetaM (Array UnifProblem)))

Equations

• One or more equations did not get rendered due to their size.

def DUnif.jpProjection (F : Lean.Expr) (p : UnifProblem) (eq : UnifEq) : Lean.MetaM (Array UnifProblem)

F is a metavariable

Equations

• One or more equations did not get rendered due to their size.

def DUnif.huetProjection (F : Lean.Expr) (p : UnifProblem) (eq : UnifEq) : Lean.MetaM (Array UnifProblem)

F is a metavariable

Equations

• One or more equations did not get rendered due to their size.

def DUnif.imitForall (F : Lean.Expr) (p : UnifProblem) (eq : UnifEq) : Lean.MetaM (Array UnifProblem)

F is a metavariable

Equations

• One or more equations did not get rendered due to their size.

def DUnif.imitProj (F : Lean.Expr) (nLam : Nat) (iTy oTy : Lean.Expr) (name : Lean.Name) (idx : Nat) (p : UnifProblem) (eq : UnifEq) : Lean.MetaM (Array UnifProblem)

F is a metavariable

Equations

• One or more equations did not get rendered due to their size.

def DUnif.imitation (F g : Lean.Expr) (p : UnifProblem) (eq : UnifEq) : Lean.MetaM (Array UnifProblem)

F is a metavariable, and g is a constant Suppose · The unification equation is (fun bin_F => F t₁ t₂ ⋯ tₙ) = (fun bin_g => g s₁ s₂ ⋯ sₘ) · F is of type ∀ (x₁ : α₁) ⋯ (xₖ : αₖ), β · g is of type ∀ (y₁ : γ₁) ⋯ (yₗ : γₗ), δ Then the binding for F should be binding := fun (x₁ : α₁) ⋯ (xₖ : αₖ) => g (?H₁ ⋯) (?H₂ ⋯) ⋯ (?Hₕ ⋯) Since the unification equation is eta-expanded, we have · k ≤ n, l ≤ m If we plug the binding into the original unification equation and headbeta the left-hand side, we will see that h + n - k - len(bin_F) = m - len(bin_g), i.e. · h = m + k + len(bin_F) - n - len(bin_g) The above equation can be used to determine the value of h.

Now we specify the types of fresh metavariables and the resulting equations · The type of ?Hᵢ (1 ≤ i ≤ min (l, h)) is taken care of by forallMetaTelescopeReducing · If h ≤ l, the type of binding should be unified with the type of F. This unification equation should be prioritized · If h > l, the type of fun (x₁ : α₁) ⋯ (xₖ : αₖ) => g (?H₁ ⋯) (?H₂ ⋯) ⋯ (?Hₗ ⋯) should be unified with ∀ (z₁ : ?η₁) ⋯ (zₙ : ?ηₕ₋ₗ), β. This unification equation should be prioritized. Moreover, the type of ?Hᵢ should be obtained by calling forallMetaTelescope on ∀ (z₁ : ?η₁) ⋯ (zₙ : ?ηₕ₋ₗ), β

Equations

• One or more equations did not get rendered due to their size.

def DUnif.elimination (F : Lean.Expr) (p : UnifProblem) (eq : UnifEq) : Lean.MetaM (Duper.LazyList (Lean.MetaM (Array UnifProblem)))

Equations

• One or more equations did not get rendered due to their size.

def DUnif.identification (F G : Lean.Expr) (p : UnifProblem) (eq : UnifEq) : Lean.MetaM UnifRuleResult

Both F and G are metavariables Proposal Premises F : (x₁ : α₁) → (x₂ : α₂) → ⋯ → (xₙ : αₙ) → β x₁ x₂ ⋯ xₙ (F : ∀ [x], β [x]) G : (y₁ : γ₁) → (y₂ : γ₂) → ⋯ → (yₘ : γₘ) → δ y₁ y₂ ⋯ yₙ (G : ∀ [y], δ [y])

Binding η : ∀ [x] [y], Type ?u H : ∀ [x] [y], η [x] [y] F ↦ λ [x]. H [x] (F₁ [x]) ⋯ (Fₘ [x]) G ↦ λ [y]. H (G₁ [y]) ⋯ (Gₙ [y]) [y] Extra Unification Problems: λ[x]. η [x] (F₁ [x]) ⋯ (Fₘ [x]) =? λ[x]. β [x] λ[y]. η (G₁ [y]) ⋯ (Gₙ [y]) [y] =? λ[y]. δ [y] Side condition: F cannot depend on G, and G cannot depend on F. If any of F or G depends on another, switch to elimination

Equations

• One or more equations did not get rendered due to their size.