Skip to content

Instantly share code, notes, and snippets.

@bhaktishh

bhaktishh/MoreBasic.sexp Secret

Created December 27, 2022 08:54
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 bhaktishh/66a6eefc0cc2c75fa70fb5abb7dbff9e to your computer and use it in GitHub Desktop.
Save bhaktishh/66a6eefc0cc2c75fa70fb5abb7dbff9e to your computer and use it in GitHub Desktop.
Download ZIP
Example s-expression & code
Raw
MoreBasic.sexp
((v((control())(attrs())(expr(VernacInductive Inductive_kw((((false(((v(Id Bool2))(loc(((fname(InFile(dirpath())(file ./MoreBasic.v)))(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 10)(ep 15)))))()))(()())(((v(CSort(UAnonymous(rigid true))))(loc(((fname(InFile(dirpath())(file ./MoreBasic.v)))(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 18)(ep 22))))))(Constructors((false(((v(Id tru))(loc(((fname(InFile(dirpath())(file ./MoreBasic.v)))(line_nb 2)(bol_pos 26)(line_nb_last 2)(bol_pos_last 26)(bp 30)(ep 33)))))((v(CHole()IntroAnonymous()))(loc(((fname(InFile(dirpath())(file ./MoreBasic.v)))(line_nb 2)(bol_pos 26)(line_nb_last 2)(bol_pos_last 26)(bp 33)(ep 33)))))))(false(((v(Id fls))(loc(((fname(InFile(dirpath())(file ./MoreBasic.v)))(line_nb 3)(bol_pos 34)(line_nb_last 3)(bol_pos_last 34)(bp 38)(ep 41)))))((v(CHole()IntroAnonymous()))(loc(((fname(InFile(dirpath())(file ./MoreBasic.v)))(line_nb 3)(bol_pos 34)(line_nb_last 3)(bol_pos_last 34)(bp 41)(ep 41))))))))))()))))))(loc(((fname(InFile(dirpath())(file ./MoreBasic.v)))(line_nb 1)(bol_pos 0)(line_nb_last 3)(bol_pos_last 34)(bp 0)(ep 42)))))
Raw
MoreBasic.v
Inductive Bool2 : Type :=
| tru
| fls.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment