Skip to content

Instantly share code, notes, and snippets.

@donovancrichton

donovancrichton/CantPatternMatchOnDPair.idr

Created September 2, 2022 03:24
Show Gist options
  • Save donovancrichton/b623cb4a3983d447186218cd1a828fcd to your computer and use it in GitHub Desktop.
Save donovancrichton/b623cb4a3983d447186218cd1a828fcd to your computer and use it in GitHub Desktop.
Download ZIP
Non-covering case when pattern matching on dependent pair.
Raw
CantPatternMatchOnDPair.idr
module CantPatternMatchOnDPair
%default total
data Expr : Type -> Type where
Lam : {a, b : Type} -> (a -> Expr b) -> Expr (a -> b)
-- this should be covering
f : (a : Type ** Expr a) -> (b : Type ** Expr b)
f (ty ** focus) =
case focus of
(Lam f) => ?look_0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment