Skip to content

Instantly share code, notes, and snippets.

@sstucki
sstucki / TransRel.agda
Created December 8, 2017 11:10
Convenient reasoning about transitive relations
-- In response to https://lists.chalmers.se/pipermail/agda/2017/009872.html
module _ where
open import Data.Product using (proj₁; proj₂)
open import Level using (suc; _⊔_)
open import Relation.Binary
------------------------------------------------------------------------
-- Transitive relations that are not necessarily reflexive
@sstucki
sstucki / CoercionsAsInstances.agda
Created December 17, 2020 17:45
Implementing coercions through instances in Agda
-- An attempt to implement implicit coercions via Agda's instance
-- argument resolution. The basic principle works, but Agda's
-- instance resolution is a bit too weak to scale it to big examples
-- because it is hard to implement chains of coercions.
-- Doesn't help: {-# OPTIONS --overlapping-instances #-}
record Coercion {a} (x y : Set a) : Set a where
constructor ⌞_⌟
field coe : x → y