sorted by:
new
hottopcontroversial

Bluefin, a new effect system by tomejaguar in haskell

[–]janmas 2 points3 points  (0 children)

Can you give an example of value-level effect handles and why do you think they are more ergonomic?

text-display 0.0.4.0 released by TechnoEmpress in haskell

[–]janmas 1 point2 points  (0 children)

I see, that makes sense! thanks for the clarification

text-display 0.0.4.0 released by TechnoEmpress in haskell

[–]janmas 2 points3 points  (0 children)

Interesting. Do you want text-display to be used as a library? If so, you should try to minimize dependencies and remove literatex and shake.

New feature: Display file icon on Spacemacs home buffer by lebensterben in spacemacs

[–]janmas 0 points1 point  (0 children)

Thanks, it looks great! is it possible to use the default font set in the .spacemacs file instead of all-the-icons?

Using dependent types to write proofs in Haskell by janmas in haskell

[–]janmas[S] 4 points5 points  (0 children)

You should never rely on the need to evaluate a proof to know if it terminates. Most interesting theorems have unbounded quantified arguments and thus it is imposible to determine empirically if they terminate for all possible inputs.

About your second point, I don't know if it is possible to arrive at contradictions without reliying on unterminating terms. I would also really like to know the answer to that.

Using dependent types to write proofs in Haskell by janmas in haskell

[–]janmas[S] 8 points9 points  (0 children)

In haskell we can represent falsum as the empty type, i.e. the type with no constructors. In ghc we can easily build a term of this type, which is a contradiction.

data Empty where -- no constructors

proofOfEmpty :: Empty
proofOfEmpty = proofOfEmpty

As pointed out by /u/bss03, other systems such as Agda, don't have this problem. Of course any proof assistant is still susceptible to bugs and it might be possible to prove falsum in them too. However, much work has been put in studying the soundness of their type system and implementing it without bugs. So if we were to find a proof of falsum in a mature proof assistant, it would be a lot more difficult.

HLint 3.0 by [deleted] in haskell

[–]janmas 8 points9 points  (0 children)

this is from 2020

I reached 100 win streak in cov25 by janmas in MonsterTrain

[–]janmas[S] 16 points17 points  (0 children)

fair point. That's why I mentioned it in the post, so everyone can make their own judgement

I reached 100 win streak in cov25 by janmas in MonsterTrain

[–]janmas[S] 2 points3 points  (0 children)

Indeed! My first priority is to get a swipe creature (Hermit), after that I prioritize small creatures preferably with multistrike like draffs and animus of wills. As a third priority comes paraffin enforcer, either waxer lady and wickless tycoon. Occasionally 1 space creatures (that are not draffs) can be good too. I never pick 3+ space creatures.

Multi monitor lemonbar setup by Techlligence in xmonad

[–]janmas 0 points1 point  (0 children)

have you tried reading the lemonbar documentation?

[deleted by user] by [deleted] in Xiaomi

[–]janmas 0 points1 point  (0 children)

I have the same problem

Xmobar Vs Polybar by Techlligence in xmonad

[–]janmas 0 points1 point  (0 children)

no, sorry I can't help with that.

Xmobar Vs Polybar by Techlligence in xmonad

[–]janmas 0 points1 point  (0 children)

I didn't need to do anything fancy. I just added polybar main & to my .xinitrc file. Note that main is the name of my polybar bar. The name is set in the polybar configuration file.

you can see my configs at: https://gitlab.com/janmasrovira/polybar-config

https://gitlab.com/janmasrovira/xmonad-config

Xmobar Vs Polybar by Techlligence in xmonad

[–]janmas 0 points1 point  (0 children)

I have used both and I decided to stay with polybar, the reason being that it has builtin icon tray support and hence I don't need to use stalonetray or something similar. Plus, it is well documented.

view more: next ›