simplify dependent Message code slightly

sullyj3 · Jul 29, 2024 · c2fdbea · c2fdbea
1 parent a520477
commit c2fdbea
Showing 1 changed file with 3 additions and 9 deletions.
diff --git a/src/Sand/Message.lean b/src/Sand/Message.lean
@@ -40,28 +40,22 @@ inductive ResumeTimerResponse
  | alreadyRunning
  deriving Repr, ToJson, FromJson
 
-def ResponseFor : Command → Type
+abbrev ResponseFor : Command → Type
  | .addTimer _ => AddTimerResponse
  | .list => ListResponse
  | .cancelTimer _ => CancelTimerResponse
  | .pauseTimer _ => PauseTimerResponse
  | .resumeTimer _ => ResumeTimerResponse
 
 def toJsonResponse {cmd : Command} (resp : ResponseFor cmd) : Lean.Json := by
- cases cmd <;> (
- simp only [ResponseFor] at resp
- exact toJson resp
- )
+ cases cmd <;> exact toJson resp
 
 def serializeResponse {cmd : Command} (resp : ResponseFor cmd) : ByteArray :=
  String.toUTF8 <| toString <| toJsonResponse resp
 
 def fromJsonResponse? {cmd : Command}
  (resp : Json) : Except String (ResponseFor cmd) := by
- cases cmd <;> (
- simp only [ResponseFor]
- exact fromJson? resp
- )
+ cases cmd <;> exact fromJson? resp
 
 
 end Sand