Conversation

Notices

1. nikki (nik@letsalllovela.in)'s status on Wednesday, 18-Aug-2021 20:55:51 JST nikki

   • pounce
   @pie @pounce ive been stuck with reflection and weird interface hill and i would like a moment off mr bones wild ride
   • pounce (pounce@nyan.network)'s status on Wednesday, 18-Aug-2021 20:55:49 JST pounce

     in reply to

     • バツ子（痛いの痛いの飛んでけ;;
     • pounce
     @nik @pie @shmibs source: https://git.sr.ht/~pounce/Santorini/tree/master/item/Santorini/Prelude.lean#L41and usage: https://git.sr.ht/~pounce/Santorini/tree/master/item/Santorini/Board.lean#L18i'd like to see go do that
   • pounce (pounce@nyan.network)'s status on Wednesday, 18-Aug-2021 20:55:50 JST pounce

     in reply to

     • バツ子（痛いの痛いの飛んでけ;;
     @nik @pie @shmibs omg this reminds me of a macro i wrote in Lean that would autogen a ton of methods and json marshall/unmarshalling code from a list of enum names
   • nikki (nik@letsalllovela.in)'s status on Wednesday, 18-Aug-2021 20:55:51 JST nikki

     in reply to

     • pounce
     @pie @pounce *hell
   • nikki (nik@letsalllovela.in)'s status on Wednesday, 18-Aug-2021 20:55:51 JST nikki

     in reply to

     • バツ子（痛いの痛いの飛んでけ;;
     • pounce
     @pie @pounce oh and don't forget codegen@shmibs just implemented https://github.com/alvaroloes/enumer in our work backend. it's *nice* but also.......feels very hacky still.
   • バツ子（痛いの痛いの飛んでけ;; (shmibs@tomo.airen-no-jikken.icu)'s status on Wednesday, 18-Aug-2021 20:56:11 JST バツ子（痛いの痛いの飛んでけ;;

     in reply to

     • pounce
     @pounce @pie @nik ah lean ^^swapping email recently with maths phd 幼馴染 about it because got all excited seems kind of the first step towards bridging the CS and Real Maths rift
   • nikki (nik@letsalllovela.in)'s status on Wednesday, 18-Aug-2021 20:56:12 JST nikki

     in reply to

     • バツ子（痛いの痛いの飛んでけ;;
     • pounce
     @pounce @pie @shmibs okay ignoring that wtf is this syntax
   • pounce (pounce@nyan.network)'s status on Wednesday, 18-Aug-2021 20:56:12 JST pounce

     in reply to

     • バツ子（痛いの痛いの飛んでけ;;

     @nik @pie @shmibs in short it’s supposed to look like haskell but also every tiny bit of it at every stage of code elaboration and parsing and generating is overridable at runtime which is awesome also all unicode is supported

     in dependent type theory you usually have lots of things that have the form “x:T + proof x is something” which is a “subset type” of T Fin n is a finite subset of the naturals of numbers less that n so the type is literally “number + proof number is less than n” that’s what the angly brackets are, and the things past the commas in the brackets are my proofs that the numbers are truly less than what they say they are

     it’s like zero cost abstractions on steroids (this all compiles to very efficient C, where allOf 10 would just compile to an array of 0-9)