CodingCellist

> It's android with racket chez fork, no root On mobile, that's cool! :eyes: IIRC, @Z-snails had success with that? : )

Seems to partially repro on the latest Yaffle: ``` $ yaffle Issue3023.yaff [...] Version 0.8.0-5b89c7ed6 1/1: Building Issue3023 (Issue3023.yaff) Issue3023> boom \eq => 3 ++ [()] Issue3023> :set showtypes Issue3023>...

@freddi301 I really like the idea of the "opinionated setup for the hasty" note, followed by a nobrainer script! : ) EDIT: I would include some bullet-points describing what the...

This seems abandoned? There also seems to have been a question as to whether the change preserved the pedagogy. Closing in 1 week (Thursday 13 Nov UTC+0) unless there is...

Shrunk further: ```idris decFn : (x : Char) -> Dec (x === ' ') -> () decFn ' ' (Yes Refl) = ?decFn_rhs_0 decFn x (No contra) = ?decFn_rhs_1 -----...

> Should I check different versions of Racket while compiling "idris2_app/idris2-boot.rkt" If you can install a newer version of Racket, I would try that yes. From a bit of searching...

Another keymasher here 👋 I do think elseLuna raise a good point: how would unique holes interact with the REPL? Part of the strength of holes (imo) is to be...

> # Environment > > macOS on M4 chip > > Idris 2, version 0.7.0 If possible, could you please try with version 0.8.0? There were a couple of significant...