This repository has no description www.jonmsterling.com/01HC/
dependent-types proof-assistant swift
3

Configure Feed

Select the types of activity you want to include in your feed.

A comment

Jon Sterling (Mar 14, 2026, 12:51 PM UTC) df0eff5c 55e0d858

+1 -1
+1 -1
Sources/PterodactylCore/Unification/Solve.swift
··· 182 182 } 183 183 184 184 extension MetaSink { 185 - // What happened to `level`? 186 185 func solveMeta(level: Int, metaName: QName, spine: Value.Spine, rhs: TypedValue) async throws(UnifyError) { 186 + // Perhaps if the meta is already solved we should unify the two solutions. 187 187 guard let meta = await meta(named: metaName), meta.solution == nil else { return } 188 188 let metaType = Evaluator(globalEnv: self, localEnv: []).evaluate(type: meta.type) 189 189