nicolabotta

Turning page time

3

Thanks for providing rmview! The application works fine with my rM 1 (version 2.12) and Debian stable. The writing speed is very good on my old Thinkpad x230 but it...

Strange color rendering

5

Thanks for providing rmview, it's a great tool! I was wandering whether color rendering is supported. I have played a bit around and I get some weird result. Writing in...

Thanks for providing rmapi! Trying to build on Debian stable: `Linux cirrus 4.19.0-18-amd64 #1 SMP Debian 4.19.208-1 (2021-09-29) x86_64 GNU/Linux` fails with ``` nicola@cirrus:~$ GO111MODULE=on go get github.com/juruen/rmapi@latest build github.com/juruen/rmapi:...

Bad syntax highlighting of .lidr files

3

Syntax highlighting works fine on .idr files but on .lidr files (Bird style), I get something like this:  Is there a way to get the same highlighting on .idr...

The program ``` > %default total > %access public export > %auto_implicits off > interface Functor F => VeriFunctor (F : Type -> Type) where > > mapPresId : {X...

The program ``` > import Data.List > %default total > %auto_implicits off > %access public export > NaturalTransformation : {F, G : Type -> Type} -> > (Functor F, Functor...

The following two files ``` > module HList.HList > %default total > %access public export > %auto_implicits off > ||| An heterogenous list (a list of values of possibly different...

Double IEEE constants: infinity, NaN, epsilon ... where are they?

1

Is there a way of accessing these values in Idris 2? Something like `Numeric.IEEE`in Haskell? At lest `epsilon`, `infinity` and `NaN` are badly needed, e.g., to implement interval arithmetics! Thanks,...

Unexpected run-time complexity

13

The program ``` import Data.Fin import Data.Vect tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A) tail f...

Cycle detected in solution of metavariable:

3

I am not sure how to reproduce this in a small, self-contained example but you should be able to download https://gitlab.pik-potsdam.de/botta/Idris2Libs and then do: ``` idris2 FiniteAsSigmaType/Properties.idr ``` in the...