Merge Vol1 and Vol2 into a single module

Author: simnalamburt

SoftwareFoundations.lean

@@ -0,0 +1,8 @@
+-- This module serves as the root of the `SoftwareFoundations` library.
+-- Import modules here that should be built as part of the library.
+
+-- Vol1
+import SoftwareFoundations.Basics
+
+-- Vol2
+import SoftwareFoundations.Equiv

SoftwareFoundationsVol1/Basics.lean renamed to SoftwareFoundations/Basics.lean

@@ -1,3 +1,7 @@
+-- Basics: Functional Programming in Coq
+--
+-- https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html
+
 -- # Data and Functions
 
 -- ## Days of the Week

SoftwareFoundations/Equiv.lean

@@ -0,0 +1,3 @@
+-- # Behavioral Equivalence
+
+-- ## Definitions

SoftwareFoundations/Imp.lean

@@ -0,0 +1,57 @@
+-- Imp: Simple Imperative Programs
+--
+-- https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html
+
+-- # Arithmetic and Boolean Expressions
+
+-- ## Syntax
+-- TODO
+
+-- ## Evaluation
+-- TODO
+
+-- ## Optimization
+-- TODO
+
+-- # Coq Automation
+
+-- ## Tacticals
+-- TODO
+
+-- ## Defining New Tactics
+-- TODO
+
+-- ## The `lia` Tactic
+-- TODO
+
+-- ## A Few More Handy Tactics
+
+-- # Evaluation as a Relation
+-- TODO
+
+-- ## Inference Rule Notation
+-- TODO
+
+-- ## Equivalence of the Definitions
+-- TODO
+
+-- ## Computational vs. Relational Definitions
+-- TODO
+
+-- # Expressions With Variables
+
+-- ## States
+-- TODO
+
+-- ## Syntax
+inductive AExp : Type
+  | ANum (n : Nat)
+  | AId (x : String) -- NEW
+  | APlus (a1 a2 : AExp)
+  | AMinus (a1 a2 : AExp)
+  | AMult (a1 a2 : AExp)
+
+def w : String := "W"
+def x : String := "X"
+def y : String := "Y"
+def z : String := "Z"

SoftwareFoundationsVol1.lean

@@ -1,9 +1,6 @@
 name = "software-foundations-lean"
 version = "0.1.0"
-defaultTargets = ["SoftwareFoundationsVol1", "SoftwareFoundationsVol2"]
+defaultTargets = ["SoftwareFoundations"]
 
 [[lean_lib]]
-name = "SoftwareFoundationsVol1"
-
-[[lean_lib]]
-name = "SoftwareFoundationsVol2"
+name = "SoftwareFoundations"