luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

WIP

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-02-18 17:57:27 -06:00
parent cd9182ca5f
commit fcccd9443a
2 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
prototyping/.gitignore vendored
View file

@ -3,4 +3,7 @@
Main
MAlonzo
PrettyPrinter
Interpreter
!Tests/Interpreter
!Tests/PrettyPrinter
.ghc.*

12
prototyping/Properties/Product.agda Normal file
View file

@ -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)