Ancestors

Toot

Written by James Wood on 2024-10-12 at 11:39

In Coq/Rocq, we abstract common patterns in Gallina using Definition, and common patterns in Ltac using Ltac. How do we abstract common patterns in Vernacular?

=> More informations about this toot | More toots from mudri@mathstodon.xyz

Descendants

Written by Yannick Forster on 2024-10-12 at 11:55

@mudri MetaCoq Run? :)

=> More informations about this toot | More toots from yforster@types.pl