: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~
@fennel oh?
@rosen thankyou!
*cuddles the egg*
THIS CRITTER IS KILLLING ME. It's a sea slug that has converged on a fish shape.
Here's a vid of it swimming https://vimeo.com/159589650
It's "pectoral fins" are Rhinophores, basically antenna for smelling. It hunts jellyfish, and uses the remnant of its Foot to stick to them.
@er1n I hadn't heard of Nature style before, but I just looked it up and that's so so so much more sensible
@loki sleep well!
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
)