Show newer

@lucidiot@tiny.tilde.website @BatElite this is just lambda calculus, which you don't need to know.

In haskell, the way to express the same thing is a little more simple:

(λf x → f x)

(or without special unicode: (\f x -> f x) )

@lucidiot@tiny.tilde.website @BatElite that isn't correct

(λf . (λx . (f x))

is an expression that basically means "if I'm given a function, called f, and a value, called x, then I will apply that function to the value"

so if I wrote (λf . (λx . (f x)) (addFive) (3), the expression means "run addFive on 3", so we'll get a result of 8

(of course this is a completely useless transformation, I could just directly write "addFive 3")

:technologist_g1: 

@g I've found that a bit difficult in idris too...

problem, tumblr, porn kinda, may contain lewd words 

@lottie jeez...

:technologist_g1: 

@g the first - because I *think* (not certain) that the nodes function can be shown to be monotonically decreasing the size of the data structure, and coq might by deriving that proof automatically

:technologist_g1: 

@g does coq assume inductive types are finite?

I'm listening to a dubstep mix that I censored a track out of, and I'm... impressed I managed to censor any of it at all given that this section of the mix has FOUR different songs playing at once

@tindall@cybre.space oh dear, I'm sorry you had such a long day

*offers gentle hugs*

Show older
Computer Fairies

Computer Fairies is a Mastodon instance that aims to be as queer, friendly and furry as possible. We welcome all kinds of computer fairies!