2 ms·
Are there any formatters that detect related things and put them in the same column? Here's a Pie example: (claim Tuple3 (-> U U U
by RedNifre 2y ago
Are there any formatters that detect related things and put them in the same column? Here's a Pie example:
(claim Tuple3 (-> U U U U))
(define Tuple3 (lambda ( a b c )
(Pair a (Pair b c) )))
(claim tuple3Of (Pi ( (A U) (B U) (C U))
(-> A B C
(Tuple3 A B C ))))
(define tuple3Of (lambda ( A B C )
(lambda ( a b c )
(the (Tuple3 A B C )
(cons a (cons b c)) ))))
(claim Tuple5 (-> U U U U U U))
(define Tuple5 (lambda ( a b c d e )
(Pair a (Pair b (Pair c (Pair d e))))))
(claim tuple5Of (Pi ((A U) (B U) (C U) (D U) (E U))
(-> A B C D E
(Tuple5 A B C D E ))))
(define tuple5Of (lambda ( A B C D E )
(lambda ( a b c d e )
(the (Tuple5 A B C D E )
(cons a (cons b (cons c (cons d e))))))))