Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/hints.v

Created May 10, 2020 14:51
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Blaisorblade/dcec83b33a6b195e3ebcd9abb3a90029 to your computer and use it in GitHub Desktop.
Save Blaisorblade/dcec83b33a6b195e3ebcd9abb3a90029 to your computer and use it in GitHub Desktop.
Download ZIP
two identical Coq hints
Raw
hints.v
(*external*) (simple apply @label_pair_iapprox_persistent)(level 1, pattern
@Persistent (uPredI (iResUR ?Σ))
(@iapprox ?Σ ?Hdlang (prod label ?A)
(@label_pair_iapprox ?Σ ?Hdlang ?A ?B)
?x ?y), id 0)
simple apply @label_pair_iapprox_persistent(level 1, pattern
@Persistent (uPredI (iResUR ?META11068))
(@iapprox ?META11068 ?META11069 (prod label ?META11070)
(@label_pair_iapprox ?META11068 ?META11069 ?META11070 ?META11071)
?META11073 ?META11074), id 0)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment