commit 3ec2dfa43150c52a8d0b85afd52872a0c6a41aa2
parent 5296774b9a00cd316fb3b7274e5edf2ea5b717de
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 5 Oct 2016 10:32:53 -0400
drop [⊢ [e-stx]] ⇐-conclusion since it causes ambiguity and is undocumented
Diffstat:
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
@@ -308,7 +308,7 @@
[⊢ [e-stx props:⇒-props/conclusion]])
#:with :last-clause #'[⊢ [_ ≫ e-stx . props]]]
;; ⇐ conclusion
- [pattern (~or [⊢ [e-stx]] [⊢ (~and e-stx (~not [_ ≫ . rst]))])
+ [pattern [⊢ (~and e-stx (~not [_ ≫ . rst]))]
#:with :last-clause #'[⊢ [_ ≫ e-stx ⇐ : _]]]
[pattern (~or [⊢ pat* ≫ e-stx ⇐ τ-pat]
[⊢ pat* ≫ e-stx ⇐ : τ-pat]