Follow

So here is it. Some formalization of/around symbolic dynamics in Coq:

https://git.sr.ht/~amiloradovsky/symbolic-dynamics

Not much really. But feel free to ask questions, give advice, and/or reuse.

@amiloradovsky in some case, a straightforward git push may take up to 25s :/ i don’t think this is related to resource constrain in this case (there is an unanswered issue about that)

Anyway sourcehut remains a very cool projet nonetheless!

@lthms Hmm… I haven't noticed that big delays so far.

Just added .build.yml for the CI, and been informed right in the Git output that build started, with the link to the job.

Can't this be somehow related to the delays in your case? Something in dispatch maybe? IDK, I'm still learning.

@amiloradovsky At least I was able to understand parts of the DeMorgan file...

@amiloradovsky

"Let is_identity_map {X: Type} (f: X -> X) := forall x: X, f x = x."

Do I read this as:

Now I define is_identity_map to be (btw X denotes some kinda type) a function taking an X and yielding an X, and this function shall be so that any particular X (let's call it x) stuffed into its eating hole will be shat out untouched?

And identity map is the map which doesn't do anything to the argument, but just passes it as-is.

- identity is a map, from a type to itself (type is a parameter)

- reflexivity is a relation, on a pair of a type and it again

@amiloradovsky

I'm glad you shared the stuff. Finally I got an opening into #coq. Just let me know (or stop replying?) if you find my questions tedious.

Let swap {X Y Z: Type} (f: X -> Y -> Z) := fun x y => f y x.

Is this:

Defining swap (btw, here be types) as a function from types to types, if x y are functions you can input them to this function?

"X -> Y -> Z" why isn't this something like "X,Y -> Z"?

@byllgrim No, I'm glad to answer any questions about topics I'm passionate about.

This "swap" works on values of types X and Y respectively, not functions: takes a function from X and Y (in that order) and returns another, from Y and X (in that order).

There is a pair type X * Y, but it isn't as basic as just currying, and thus rarely used in practice.

~lthms@lthms@mastodon.social@amiloradovsky glad to see other folks using sourcehut \o/ out of curiosity, do you also have some trouble with low ssh performance?