 |
Post AvLnLTRqyhjvzStySW by [email protected] |
 |
More posts by [email protected] |
|
Post #AvLnLSAnicVO2HuqEy by [email protected] |
|
0 likes, 0 repeats |
|
|
|
No matter what you think the performance bottleneck of your proof assistant is,… |
|
|
|
Post #AvLnLSIFGwSaPNOmqO by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@totbwf No, really, it's that it doesn't even try to do algebra. |
|
|
|
Post #AvLnLSOctDZ2jANsn2 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@pigworker Unfortunately, the floor is low enough that one UNPACK pragma is abl… |
|
|
|
Post #AvLnLSUeWoNv1rChBQ by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@totbwf God preserve me from ever needing to know what that means. |
|
|
|
Post #AvLnLSb295UNLeBn84 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@pigworker @totbwf One of you is talking about the performance bottleneck as me… |
|
|
|
Post #AvLnLSi7ij9zhdVSBE by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@JacquesC2 @pigworker @totbwf few years ago I supervised an MSc project which w… |
|
|
|
Post #AvLnLSpZH37C4izOme by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@dimpase @JacquesC2 @pigworker @totbwf One often has to dance around the proof … |
|
|
|
Post #AvLnLSweqgmoQiJ3po by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@andrejbauer @dimpase @pigworker @totbwf If the dance involves one (or more?) i… |
|
|
|
Post #AvLnLT2gUHbgjP7sEC by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@JacquesC2 @andrejbauer @pigworker @totbwf for the most complicated case (a 1-l… |
|
|
|
Post #AvLnLT946Yi93C6yAq by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@dimpase @andrejbauer @pigworker @totbwf Not surprised. It's an explicit de… |
|
|
|
Post #AvLnLTFRipobMz647U by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@JacquesC2 @andrejbauer @pigworker @totbwf yeah, that was my conclusion, in hin… |
|
|
|
Post #AvLnLTLTMQdTffusVs by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@dimpase @andrejbauer @pigworker @totbwf Unfortunately, not yet, that I'm a… |
|
|
|
Post #AvLnLTRqyhjvzStySW by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@JacquesC2 @andrejbauer @pigworker @totbwf does one do bootstrapping of the kin… |
|
|
|
Post #AvLnLTYwYLPYLSDdVg by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@dimpase @JacquesC2 @andrejbauer @pigworker @totbwf MetaRocq's extraction i… |
|
|
|
Post #AvLnLTgk5LeKjdrrfM by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@dimpase @JacquesC2 @andrejbauer @pigworker @totbwf But yeah I agree with @Jacq… |
|
|
|
Post #AvLnLTn7hckn3Qqxc0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@mevenlennonbertrand @dimpase @andrejbauer @pigworker @totbwf Hmm, 'very ca… |
|
|
|
Post #AvLnLTsnMXI5L1VUS8 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@JacquesC2 @mevenlennonbertrand @dimpase @pigworker @totbwf Nobody ever wtites … |
|
|
|
Post #AvLnLTyp086xdiKIqW by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@andrejbauer writes "Nobody ever writes proof terms. Agda is just pretendi… |
|
|
|
Post #AvLnLU5uZlmZzhdxtg by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo @andrejbauer yeah adhering strongly to only using where is essen… |
|
|
|
Post #AvLnLUCIC2t2JUd3qK by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ToucanIan @MartinEscardo @andrejbauer The unifier might have some opinions on … |
|
|
|
Post #AvLnLUHxqxQKb5HagS by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@totbwf@types says 'The unifier might have some opinions on this being &quo… |
|
|
|
Post #AvLnLUP3Qb5wx4bFjc by [email protected] |
|
0 likes, 0 repeats |
|
|
|
I said "This is because the unifier doesn't follow the mathematical ar… |
|
|
|
Post #AvLnM3KJaD6HGVeShs by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo Haha! That's such an Agda perspective. The Rocq unifer is a … |
|
|
|
Post #AvLnM3PdGRLzX08hzk by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@pigworker But Rocq people hardly write terms anyway (complete or incomplete). |
|
|
|
Post #AvLnM7KShbavg7kdUW by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo They still "refine" in ways which create unification p… |
|
|
|
Post #AvLnM8LCwJmkoj6kIC by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo There is an entire Rocq industry perched on quirks of the unific… |
|
|
|
Post #AvLnMAQbBFHnI1e4yO by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo @pigworker I do quite a bit, and I almost never use tactics to c… |
|
|
|
Post #AvLnMHAY7JbiCHBrQe by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo @andrejbauer https://martinescardo.github.io/TypeTopology/UF.Equ… |
|
|
|
Post #AvLnMHILeJqUaSq5aK by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@amy@MartinEscardo @andrejbauer Now I'm curious if it would be feasible to … |
|
|
|
Post #AvLnMHPRDxW6wS9kdU by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@jesper What exactly do you mean by "erased"? |
|
|
|
Post #AvLnMNrJFFNOwdF5ua by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo @jesper it assumes that would be runtime-irrelevance : https://a… |
|
|
|
Post #AvLnMQsq01NiKEyrD6 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@andrejbauer I pretend (and keep my fingers crossed) that Agda figures out what… |
|
|
|
Post #AvLnMQzZaylkf88Ei0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@andrejbauer I think most people using proof assistants will agree with the fol… |
|
|
|
Post #AvLnMR5xDFsCyv7Kee by [email protected] |
|
0 likes, 0 repeats |
|
|
|
But notice that the above is not a criticism of proof assistants.I am very happ… |
|
|
|
Post #AvLnMu5bPdp6uEAxdI by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo What you write is usually called "unelaborated code" o… |
|
|
|
Post #AvLnMuCL0bD9F7KL8C by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@andrejbauer writes "The amount of work and additional processing that Agd… |
|
|
|
Post #AvLnMuJ4bYbBa0Tid6 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo The best way to misrepresent what you're saying would be to … |
|
|
|
Post #AvLnMuOkGT8Trb8FTE by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@andrejbauer I am happy to be misrepresented. |
|
|
|
Post #AvLnMzqE1j5WkH1lUu by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@dimpase @andrejbauer @pigworker @totbwf Some of the work on program-from-proof… |
|
|
|
Post #AvLnMzwxcgTZ5AB8zo by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@JacquesC2 @dimpase @pigworker @totbwf I sat through many talks about extractio… |
|
|
|
Post #AvLnN02zGHIRNqzxOC by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@andrejbauer writes "I sat through many talks about extraction of proofs f… |
|
|
|
Post #AvLnN12fYwdWT9rDX6 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@dimpase @andrejbauer @pigworker @totbwf Which reminds me, I ought to redo the … |
|
|
|
Post #AvLnN4UQkBcpA7rvii by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@dimpase asks "Is there something like basic linear algebra in Agda"I… |
