From fcccd9443a2bddf42d13a66cc50e7b206c3d5a13 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Fri, 18 Feb 2022 17:57:27 -0600 Subject: [PATCH] WIP --- prototyping/.gitignore | 3 +++ prototyping/Properties/Product.agda | 12 ++++++++++++ 2 files changed, 15 insertions(+) create mode 100644 prototyping/Properties/Product.agda diff --git a/prototyping/.gitignore b/prototyping/.gitignore index cca4f464..9dde90a5 100644 --- a/prototyping/.gitignore +++ b/prototyping/.gitignore @@ -3,4 +3,7 @@ Main MAlonzo PrettyPrinter +Interpreter +!Tests/Interpreter +!Tests/PrettyPrinter .ghc.* diff --git a/prototyping/Properties/Product.agda b/prototyping/Properties/Product.agda new file mode 100644 index 00000000..2118d577 --- /dev/null +++ b/prototyping/Properties/Product.agda @@ -0,0 +1,12 @@ +module Properties.Product where + +record Σ {A : Set} (B : A → Set) : Set where + + constructor _,_ + field fst : A + field snd : B fst + +open Σ public + +_×_ : Set → Set → Set +A × B = Σ (λ (a : A) → B)