You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We use List and Nat for stack and pointer, respectively. This means we have to handle indexing errors, which risk failing at runtime, and require either use of idris_crash/die, or (slow?) EitherT monad. If instead we use Vect n and Fin n, we can remove this problem at compile time. This would probably require changing the way we handle nested functions, but that might be a good thing on its own.
The text was updated successfully, but these errors were encountered:
We use
List
andNat
for stack and pointer, respectively. This means we have to handle indexing errors, which risk failing at runtime, and require either use ofidris_crash
/die
, or (slow?)EitherT
monad. If instead we useVect n
andFin n
, we can remove this problem at compile time. This would probably require changing the way we handle nested functions, but that might be a good thing on its own.The text was updated successfully, but these errors were encountered: