Skip to content

Instantly share code, notes, and snippets.

@ncfavier

ncfavier/with.agda

Created March 8, 2026 19:59
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save ncfavier/fe9530c4c4393d3c7cfb7e65edfce048 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save ncfavier/fe9530c4c4393d3c7cfb7e65edfce048 to your computer and use it in GitHub Desktop.
Download ZIP
Slightly surprising ill-typed with-abstraction. Is it a bug?
Raw
with.agda
postulate
X : Set
u : X
P : X → Set
Q : P u → Set
f : (p : P u) → Q p
f p with u | p
... | a | b = ?
-- f.with : (p : P u) (w : X) (p' : P w) → Q p'
-- ^^^^ 💥 p' is not a P u
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment