Estoy tratando de modelar un formulario de encuesta simple en Idris y actualmente estoy luchando con la validación de la entrada del usuario, que viene como una cadena, w.r.t. al tipo de preguntas formuladas.

Actualmente tengo los siguientes tipos:

data Question : Type where
  QCM : {numOptions : Nat}
      -> (question : String) 
      -> (qcmOptions : Vect numOptions String)
      -> (expected : Fin numOptions)
      -> Question

data Answer : (q : Question) -> Type where
   AnswerQCM : (option : Fin n) -> Answer (QCM {numOptions = n } q opts exp)

total 
isCorrectAnswer : (q : Question ) -> Answer q -> Bool
isCorrectAnswer (QCM {numOptions} question qcmOptions expected) (AnswerQCM option) = option == expected


data IsAnswer : (s : String) -> (q : Question) -> Type where
     ValidQCM : (option : Fin n) -> IsAnswer s (QCM {numOptions = n } q opts exp)

notInRange : (num : Fin n) -> { auto prf : GT numOptions n } 
           -> IsAnswer s (QCM {numOptions} q opts exp) -> Void
notInRange num x = ?notInRange_rhs

No veo como escribir elnotInRangefunción que debería ser una prueba de que algún número puede no ser una respuesta válida a una encuesta de preguntas de opción múltiple: este número debe estar en el rango correcto para el número de opciones ofrecidas dentro de la pregunta.

En general, quiero escribir unreadAnswer función que se vería así:

readAnswer : (s : String) -> (q : Question) -> Dec (IsAnswer s q)
readAnswer s (QCM question qcmOptions expected) = ?readAnswer_rhs_1

Parece que estoy teniendo dificultades para encontrar elcontra parte deDec porque mis tipos no expresan correctamente las restricciones que quiero de tal manera que algunas de ellas puedan quedar deshabitadas.