Login
From:
Thomas Letan’s website
(Uncensored)
subscribe
Ltac is an Imperative Metaprogramming Language · ~lthms
https://soap.coffee/~lthms/posts/LtacMetaprogramming.html
links
backlinks
Roast topics
Find topics
Find it!
Ltac generates terms, therefore it is a metaprogramming language. It does it incrementally, by using primitives to modifying an implicit state, therefore it is an imperative language. Henceforth, it is an imperative metaprogramming language.