Ztellman uses them in his int set

I remember reading them in his code and he was quite proud of them when he pointed them out to me

err i can't find them right now. but i know he used some in one of his libs

ah nailed it. but its in java https://github.com/clojure/data.int-map/blob/33e6baa4b30acb56ec7bb3f11265e221f07b96bb/src/main/java/clojure/data/int_map/Nodes.java#L41

i can't for the life of me remember why and how he used them. it was clever but i can't remember

I never managed getting used to slack (over gitter, for technical topics)

Seeing your mentions if you're not constantly infusing the channel into your line of sight, always seems broken in slack

What am I missing?

besides "it adds induction", what is the difference between Calculus of Constructions and Calculus of Inductive Constructions ?

@qqq your off-topic question is arguably much more intelligent than mine 🙂

@matan: I'm basically abusing #off-topic are free-consulting/tutoring, since there are so many knowledgable + helpful people here 🙂

@qqq it was meant as a compliment 🙂