def Auto.Embedding.Lam.Inhabitation.subsumeQuick (s₁ s₂ : LamSort) : Bool

Given two sorts s₁ s₂, run a quick test on whether the inhabitation of s₁ subsumes the inhabitation of s₂

Equations

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

def Auto.Embedding.Lam.Inhabitation.trivialQuick (s : LamSort) : Bool

Run a quick test on whether the inhabitation of s is trivial

Equations

• Auto.Embedding.Lam.Inhabitation.trivialQuick = Auto.Embedding.Lam.Inhabitation.trivialQuick.go Std.HashSet.emptyWithCapacity

def Auto.Embedding.Lam.Inhabitation.trivialQuick.go (argTys : Std.HashSet LamSort) (s : LamSort) : Bool

Equations

• Auto.Embedding.Lam.Inhabitation.trivialQuick.go argTys (argTy.func resTy) = (argTys.contains (argTy.func resTy) || Auto.Embedding.Lam.Inhabitation.trivialQuick.go (argTys.insert argTy) resTy)
• Auto.Embedding.Lam.Inhabitation.trivialQuick.go argTys s = argTys.contains s