Fixing PartialIf.err

agda · Dec 24, 2023 · 8378f85 · 8378f85
1 parent d6d210f
commit 8378f85
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/test/golden/PartialIf.err b/test/golden/PartialIf.err
@@ -1,2 +1,2 @@
 test/Fail/PartialIf.agda:5,1-11
-if_then_else must be fully applied
+if_then_else_ must be fully applied