-
|
From discussion #27 |
Beta Was this translation helpful? Give feedback.
Replies: 2 comments 2 replies
-
|
For great details see: #27 In short terms are in the gallina language (Coq's functional programming language and more) and tactics are in the tactic language (e.g. ltac, ltac2, mtac...). The original ASTactic model only embeds terms in Gallina as far as I know and produce tactics using the decoder and the grammar specified in the paper. Feel free to correct me if this is not an accurate summary. |
Beta Was this translation helpful? Give feedback.
-
|
Thanks! I thought there was a button to move an issue to discussions automatically. But I gave up when failing to find the button. |
Beta Was this translation helpful? Give feedback.
-
|
makes sense, I've seen a template showing up for gitissues in other projects telling ppl not to post questions as an issue, maybe you can do that? (not sure how but would be nice! :) ) I am happy to help move the other question I wrote, is that ok with you if I go ahead and do it? |
Beta Was this translation helpful? Give feedback.
-
|
Thanks, I'll take a look whenever I get a chance. |
Beta Was this translation helpful? Give feedback.
For great details see: #27
In short terms are in the gallina language (Coq's functional programming language and more) and tactics are in the tactic language (e.g. ltac, ltac2, mtac...). The original ASTactic model only embeds terms in Gallina as far as I know and produce tactics using the decoder and the grammar specified in the paper.
Feel free to correct me if this is not an accurate summary.