I hereby claim:
- I am psygnisfive on github.
- I am beka_valentine (https://keybase.io/beka_valentine) on keybase.
- I have a public key ASCQi6X54gVDWkg47lpWuAEQ8bxHMELnU6FQI1YrPWLvvwo
To claim this, I am signing this object:
Rebecca Valentine BekaValentine
BekaValentine
/ gist:e81b55f4aef1f380691096b2bff71280
Created
September 5, 2018 10:12
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Data_List :: forall r :: *. | |
| (forall list :: * -> *. | |
| (forall a. list a) -> | |
| (forall a. a -> list a -> list a) -> | |
| (forall a b. (() -> b) -> (a -> list a -> b) -> b) -> | |
| r) | |
| -> r | |
| Data_List dependee = | |
| dependee {\a -> Fix l. (forall b. (() -> b) -> (a -> l a -> b) -> b)} | |
| <scott encoded nil> |
BekaValentine
/ gist:e252ad620f9e7dd8fbd125d15b70947d
Created
September 5, 2018 14:58
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Slack bug. :( |
BekaValentine
/ gist:df581b886700fce3583a6f2ed8397367
Last active
September 8, 2018 06:08
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| grammar Var x y z == String. | |
| grammar Term M N P ::= | |
| var x, x, "variable"; | |
| zero, "zero", "zero"; | |
| suc M, "suc" M, "successor"; | |
| pair M N , "<" M "," N ">" , "pair"; | |
| fst P , "fst" P , "fst"; | |
| snd P , "snd" P , "snd"; | |
| lam x M, "\\" x "->" M, "lambda"; |
BekaValentine
/ gist:1aa6e3ec142230bb34fa28ca0cbefd32
Created
September 11, 2018 08:17
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Future Plutus Roadmap | |
| - Current Plutus | |
| ? User-friendly Documentation for Plutus | |
| ? Improved feedback from the type checker | |
| - Better error messages | |
| - Better explanations/localizations of messages | |
| - Better information on the context (both scope and syntactic context) | |
| - Better suggestion for repair | |
| - Holes?? |
BekaValentine
/ STLCWithValueInclusion.agda
Created
September 11, 2018 17:13
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module STLCWithValueInclusion where | |
| data Type : Set where | |
| Bool : Type | |
| _*_ _=>_ : Type -> Type -> Type | |
| data Context : Set where | |
| [] : Context |
BekaValentine
/ gist:f0bb68843c2f5208ef7549ba73b0cd43
Created
September 30, 2018 02:34
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Updating to “language-agda@1.0.6” failed.Hide output… | |
| > tree-sitter-agda@1.0.14 install /private/var/folders/96/kxbvkfwd2gg09z9zxd4_1bfc0000gn/T/apm-install-dir-118829-55630-m4g3pw.1qafumzpvi/node_modules/language-agda/node_modules/tree-sitter-agda | |
| > node-gyp rebuild | |
| xcode-select: error: tool 'xcodebuild' requires Xcode, but active developer directory '/Library/Developer/CommandLineTools' is a command line tools instance | |
| xcode-select: error: tool 'xcodebuild' requires Xcode, but active developer directory '/Library/Developer/CommandLineTools' is a command line tools instance |
BekaValentine
/ gist:06e3e9802011035db6f38d08045293fc
Created
October 1, 2018 09:00
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| > tree-sitter-agda@1.0.14 install /private/var/folders/96/kxbvkfwd2gg09z9zxd4_1bfc0000gn/T/apm-install-dir-11891-4804-q3a9ts.e4wph/node_modules/language-agda/node_modules/tree-sitter-agda | |
| > node-gyp rebuild | |
| gyp info it worked if it ends with ok | |
| gyp verb cli [ '/Applications/Atom.app/Contents/Resources/app/apm/bin/node', | |
| gyp verb cli '/Applications/Atom.app/Contents/Resources/app/apm/node_modules/.bin/node-gyp', | |
| gyp verb cli 'rebuild' ] | |
| gyp info using node-gyp@3.4.0 | |
| gyp info using node@8.9.3 | darwin | x64 |
BekaValentine
/ gist:a51b6acbf77f7b0ffff88133f36da8d2
Created
November 22, 2018 19:52
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| $ ping 8.8.8.8 | |
| PING 8.8.8.8 (8.8.8.8): 56 data bytes | |
| Request timeout for icmp_seq 0 | |
| Request timeout for icmp_seq 1 | |
| 64 bytes from 8.8.8.8: icmp_seq=0 ttl=120 time=2305.913 ms | |
| 64 bytes from 8.8.8.8: icmp_seq=1 ttl=120 time=1304.682 ms | |
| 64 bytes from 8.8.8.8: icmp_seq=2 ttl=120 time=304.634 ms | |
| 64 bytes from 8.8.8.8: icmp_seq=3 ttl=120 time=326.845 ms | |
| 64 bytes from 8.8.8.8: icmp_seq=4 ttl=120 time=1283.949 ms | |
| 64 bytes from 8.8.8.8: icmp_seq=5 ttl=120 time=278.704 ms |
BekaValentine
/ gist:e542fbc0dea33f10ddf0545ac8c7d16c
Created
December 13, 2018 18:34
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| hash(a,b,c) = hashToken(a)*P^2 + hashToken(b)*P + hashToken(c) |
BekaValentine
/ keybase.md
Created
March 14, 2019 18:17