Zulip Chat Archive
Stream: triage
Topic: PR !4#16267: chore(Order/RelIso/Basic): `[s : Setoid α]` ...
Random Issue Bot (Sep 30 2024 at 14:10):
Today I chose PR 16267 for discussion!
chore(Order/RelIso/Basic): [s : Setoid α] => {s : Setoid α}
Created by @FR (@FR-vdash-bot) on 2024-08-29
Labels: t-order, t-data
Is this PR still relevant? Any recent updates? Anyone making progress?
Last updated: May 02 2025 at 03:31 UTC