This commit is contained in:
Michael Zhang 2024-06-25 16:46:47 -05:00
parent a44df7d34a
commit 11d587cf2a

View file

@ -178,5 +178,5 @@ Prove that
```agda
decidable-equality-char : (A : Type) → has-decidable-equality A ⇔ has-bool-dec-fct A
decidable-equality-char = ?
decidable-equality-char = {! !}
```