<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 10pt;
font-family:Tahoma
}
--></style>
</head>
<body class='hmmessage'>
Hello,<br><br>Just wondering if this is a bug.<br><br>agda --version<br>Agda version 2.2.11<br><br>-- agda code below<br><br><br>module test where<br><br>data Bool : Set where<br> true : Bool<br> false : Bool<br><br>data ℕ : Set where<br> zero : ℕ<br> succ : ℕ → ℕ<br><br>data Type : (A : Set) → Set where<br> isBool : Type Bool<br> isℕ : Type ℕ<br><br>g : {A : Set} → Type A → Type A → ℕ<br>g (isBool) (isBool) = zero<br>g (isℕ) (isℕ) = (succ zero)<br><br><br>-- agda error message below:<br><br>/home/j/dev/apps/haskell/agda/learn/test.agda:17,1-18,28<br>Cannot split on the constructor isℕ<br>when checking the definition of g<br><br>Any thoughts, please?<br><br>Thanks<br> </body>
</html>