From 4641cf666f6905936ad1c46223c8df0c256558b3 Mon Sep 17 00:00:00 2001 From: Aaron Bembenek Date: Mon, 3 Feb 2020 10:42:53 -0500 Subject: [PATCH] Tweaks to docs. --- docs/01_language_basics.md | 2 +- docs/04_logical_formulas.md | 13 ++++++++----- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/docs/01_language_basics.md b/docs/01_language_basics.md index ad2deaab..b1887417 100644 --- a/docs/01_language_basics.md +++ b/docs/01_language_basics.md @@ -244,7 +244,7 @@ nested functions that can locally capture variables and we also support a special parameterized term `fold`: ``` -fold[f] : ['a -> 'b list] -> 'a +fold[f] : ['a, 'b list] -> 'a ``` where `f` is the name of a function of type `['a, 'b] -> 'a`. Here's an example diff --git a/docs/04_logical_formulas.md b/docs/04_logical_formulas.md index c970cd37..89b9bc78 100644 --- a/docs/04_logical_formulas.md +++ b/docs/04_logical_formulas.md @@ -138,8 +138,8 @@ thing as `#{"x"}[bool]`. ### Built-in formula terms Formulog provides built-in terms that are used to construct formulas that -should be interpreted under a particular theory. The formulas generally reflect -SMT-LIB terms. +should be interpreted under a particular theory. For the most part, these +constructors directly reflect the SMT-LIB standard. #### Parameterized terms @@ -175,10 +175,13 @@ of the bit vectors in the comparisons: In this case, one annotation is enough to clarify things: ``` -`smt_eq[bv[16]](bv_const(42), bv_const(0))` -`smt_eq(bv_const[16](42), bv_const(0))` +`smt_eq[bv[32]](bv_const(42), bv_const(0))` +`smt_eq(bv_const[32](42), bv_const(0))` ``` +The parameters to a parameterized constructor have to be fully resolved at +compile time. + #### Logical connectives Formulog has the standard first-order logic connectives: @@ -385,7 +388,7 @@ type 'a my_list = In addition to being able to use the constructors `my_nil` and `my_cons` within a formula, one can also use constructors that are automatically generated by -Formulog and that make it easier to state formula about `my_list` terms: +Formulog and that make it easier to state formulas about `my_list` terms: ``` #is_my_nil : 'a my_list smt -> bool smt