This file contains 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
# $xs->@* basically means dereference $xs as a list | |
my $xs = [1,2,3]; | |
push($xs->@*, 4); | |
say $xs->@*; # This prints 1234 | |
# That is, 4 is pushed onto the ned of the array | |
$xs = [1,2,3]; | |
my @list = $xs->@*; |
This file contains 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 peano_equal where | |
data Nat : Set where | |
z : Nat | |
s : Nat -> Nat | |
record True where | |
constructor T | |
data False where |
This file contains 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 v where | |
data Nat : Set where | |
zero : Nat | |
suc : Nat -> Nat | |
data Vec (A : Set) : Nat -> Set where | |
[] : Vec A zero | |
_::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n) |
This file contains 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
### Keybase proof | |
I hereby claim: | |
* I am NicolaiNebel on github. | |
* I am nicolainebel (https://keybase.io/nicolainebel) on keybase. | |
* I have a public key whose fingerprint is 7916 7FEA FF22 C9D7 8417 7D52 201D 6E52 0987 4217 | |
To claim this, I am signing this object: |