- MEMOCODE Paper Accepted
- NFM '21 (Virtual) Conference Presentation
- Paper Accepted to NFM '21
- Ltac Bug or Ltac Feature?
- Deep Field by Eric Whitacre
- Higher-Order Automation
- HotSoS 2020 Poster Presentation
- Dissertation Proposal Defense

Index

Blog

Blog Categories

Announcements

Coq

Music

07 Dec 2020

I encountered some surprising (to me) behavior while writing an Ltac procedure involving a “with” clause. A minimal example appears below. The problem occurs when binding a variable from a hypothesis, then using that variable in the LHS of a with binding in the Ltac body. My expectation is that the LHS (x in the assignment x:=y) is unaffected by substitution, and must simply match the name of a bound variable in the type of the Lemma to which it is being applied.

24 Nov 2020

I would like to pass a tactic as a parameter to a separately-defined Ltac procedure. However, it seems whenever I include a “;” in that tactic I’m met with a syntax error. I’ve crafted a minimal example below. Perhaps I’ve made a silly mistake with parentheses or some such, but I can’t seem to get it working.

```
Ltac my_tac tac := tac.
Lemma foo : (1 = 1 /\ 2 = 2).
Proof.
split; [reflexivity | reflexivity]. (* Succeeds as expected *)
Undo.
my_tac (split; [reflexivity | reflexivity]). (* Syntax Error? *)
Qed.
```