Skip to content

Instantly share code, notes, and snippets.

@Casteran

Casteran/dyck.v Secret

Created January 21, 2023 15:36
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 Casteran/06343a071d0a874d9200d0fe79939870 to your computer and use it in GitHub Desktop.
Save Casteran/06343a071d0a874d9200d0fe79939870 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
dyck.v
From elpi Require Import elpi.
Elpi Program parenthesis lp:{{
kind paren type.
type a, b paren.
kind nat type.
type z nat.
type s nat -> nat.
pred fill o:list paren, o: nat.
fill nil z.
fill [a|L] P:- fill L (s P).
fill [b|L] (s P) :- fill L P.
}}.
Elpi Query lp:{{
fill [a,X,a,Y] z,
fill [a,X1,X2,b] z, not( X1 = a).
}}.
Elpi Query lp:{{ fill [a,X,Y,Z,T,b] z, not( X = Y) }}.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment