Issue with syntax in tr_rev_correct


2

35

June 27, 2024

How to destruct H involving two variables


2

52

June 27, 2024

Problem with notation in CPS ceval_step extension of LF's ImpCEvalFun


2

95

May 9, 2024

How do I write a summation on Coq?


2

619

January 9, 2023

Annoying warnings when Requiring/Importing ssreflect


4

546

March 28, 2022

Notation for a coinductive type


1

499

November 4, 2021

Overload list notation


3

1007

September 27, 2021

Defining and working with trivial finite sets like {x, y, z} easily


6

728

July 8, 2021

Bug in the parser?


5

836

April 1, 2021

What determines whether a custom entry is used for printing?


5

1018

October 6, 2020

Use notation defined in module type


2

1080

May 27, 2020

Numeral Notation for `Fin.t`


4

1056

April 6, 2020

Notation substitution and identifiers


0

781

March 26, 2020

Use notations to define an embedded language inside Coq


9

2144

March 19, 2020
