suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fixed typo

Browse Source
This commit is contained in:
William J. Bowman 2015-09-23 18:08:15 -04:00
parent edea1909ec
commit d2642b1c38
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 6 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
scribblings/oll.scrbl
View File

@ -4,14 +4,13 @@
@title{OLL: Ott-like Library} @title{OLL: Ott-like Library}
@defmodule[cur/oll] @defmodule[cur/oll]
The OLL provides syntax extensions for defining programming languages as The OLL provides syntax extensions for defining programming languages as inductive data. The library
inductive data. The library is inspired by Ott, which provides an is inspired by Ott@todo{Citation needed}, which provides an language that resembles math notation for
language that resembles math notation for generating Coq definitions. generating Coq definitions. The purpose of the OLL is not to replace Ott, but to demonstrate how
The purpose of the OLL is not to replace Ott, but to demonstrate how powerful syntactic meta-programming can bring features previously only provided by external tools into
powerful syntactic meta-programming can bring features previously only the language.
provided by external tools into the language.
@defform[(define-lanugage name @defform[(define-language name
maybe-vars maybe-vars
maybe-output-coq maybe-output-coq
maybe-output-latex maybe-output-latex