about summary refs log tree commit diff
path: root/lib/Quote.mli
diff options
context:
space:
mode:
authorMalte Voos <git@mal.tc>2024-02-20 12:48:36 +0100
committerMalte Voos <git@mal.tc>2024-02-20 12:48:36 +0100
commit5252fe93e5e7ef77888c06c97de4e350dce90448 (patch)
treeda057c49ece07e6fd80ec55ad59fbf337162063a /lib/Quote.mli
parent407a2a4a0a440c41adc19fbe8b67283b7b7c65ab (diff)
downloadtoytt-5252fe93e5e7ef77888c06c97de4e350dce90448.tar.gz
toytt-5252fe93e5e7ef77888c06c97de4e350dce90448.zip
nbe: quotation
Diffstat (limited to 'lib/Quote.mli')
-rw-r--r--lib/Quote.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/Quote.mli b/lib/Quote.mli
new file mode 100644
index 0000000..c55aa8b
--- /dev/null
+++ b/lib/Quote.mli
@@ -0,0 +1,2 @@
+val quote : size:int -> Domain.value -> Syntax.tm
+val quote_ne : size:int -> Domain.ne -> Syntax.tm