open import Data.Nat
open import Data.Empty
hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
Kevin Chen kvnyijia
🌟
kvnyijia
/ FLOLAC-Razor.agda
Last active
June 11, 2021 13:03
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
| -------------------------------------------------------------------------------- | |
| -- | |
| ---- Dependently Typed Programming: Part 3 | |
| -- | |
| ---- An Intrinsically Typed Compiler | |
| -- | |
| ---- Josh Ko (Institute of Information Science, Academia Sinica) | |
| -- | |
| -------------------------------------------------------------------------------- |
kvnyijia
/ FLOLAC-STLC.lagda.md
Last active
August 19, 2020 03:17
— forked from L-TChen/FLOLAC-STLC.lagda.md
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
| -------------------------------------------------------------------------------- | |
| -- | |
| ---- Dependently Typed Programming: Part 1 | |
| -- | |
| ---- Shallow Embedding of Higher-Order Logic and | |
| ---- Deep Embedding of Propositional Logic | |
| -- | |
| ---- Josh Ko (Institute of Information Science, Academia Sinica) | |
| -- | |
| -------------------------------------------------------------------------------- |
kvnyijia
/ Chapter-1-6.hs
Last active
July 24, 2020 02:59
— forked from banacorn/Chapter-1-6.hs
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
| -- This exercise covers the first 6 chapters of "Learn You a Haskell for Great Good!" | |
| -- Chapter 1 - http://learnyouahaskell.com/introduction | |
| -- Chapter 2 - http://learnyouahaskell.com/starting-out | |
| -- Chapter 3 - http://learnyouahaskell.com/types-and-typeclasses | |
| -- Chapter 4 - http://learnyouahaskell.com/syntax-in-functions | |
| -- Chapter 5 - http://learnyouahaskell.com/recursion | |
| -- Chapter 6 - http://learnyouahaskell.com/higher-order-functions | |
| -- Download this file and then type ":l Chapter-1-6.hs" in GHCi to load this exercise |