@BatElite @lucidiot@tiny.tilde.website oh my gosh I'm giggling
@BatElite @lucidiot@tiny.tilde.website ;;)
@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?
@Fenreliania legy...
@Fenreliania eee gosh!!!
@fennel sleep well, dear deer
@Lex_Lee D::
@fennel O::
@Rosemary sleep well, rosemary~
hi I'm avery, a cute lizardsquid with 3 hearts full of love!
nonbinary ░ they/she ░ australia ░ 29yo
I post: silly lizardy nonsense, world building, conlangs, doctor who
polyam, demi, open. I love affection!
hugs and cuddles and such are ok, but everything else please ask first
languages: English • Welsh (very basic)
I have a private account, ask for access!
(some old accounts:
@gwyfyndraig
@liquid_lizsquid
)