aboutsummaryrefslogtreecommitdiffstats
path: root/src/Verilog/VerilogAST.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-02-18 12:08:15 +0000
committerYann Herklotz <git@yannherklotz.com>2020-02-18 12:08:15 +0000
commit6e290b7049fc874c32e62ab816493dc5200ebc4e (patch)
treed3b6f3f16da54f05e5d53471b7e460c2fe202865 /src/Verilog/VerilogAST.v
parent2a4153de356f8d29359c5950d1d9cbc498d7c2f3 (diff)
downloadvericert-kvx-6e290b7049fc874c32e62ab816493dc5200ebc4e.tar.gz
vericert-kvx-6e290b7049fc874c32e62ab816493dc5200ebc4e.zip
Update Verilog AST with flat array
Diffstat (limited to 'src/Verilog/VerilogAST.v')
-rw-r--r--src/Verilog/VerilogAST.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Verilog/VerilogAST.v b/src/Verilog/VerilogAST.v
index 362fe45..5886652 100644
--- a/src/Verilog/VerilogAST.v
+++ b/src/Verilog/VerilogAST.v
@@ -32,6 +32,9 @@ Inductive value : Type :=
| VBool (b : bool)
| VArray (l : list value).
+Inductive literal : Type :=
+| LitArray (l : list bool).
+
Definition cons_value (a b : value) : value :=
match a, b with
| VBool _, VArray b' => VArray (a :: b')