Last active
January 17, 2016 16:15
-
-
Save bishboria/72852a783d608c93b56d to your computer and use it in GitHub Desktop.
How do I fix the 'cannot decide' error in the opt function?
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 LittleLang where | |
open import Data.Bool | |
open import Data.Nat | |
data type : Set where | |
tNat tBool : type | |
data exp : type → Set where | |
nat : ℕ → exp tNat | |
plus : exp tNat → exp tNat → exp tNat | |
bool : Bool → exp tBool | |
and : exp tBool → exp tBool → exp tBool | |
fromType : type → Set | |
fromType tNat = ℕ | |
fromType tBool = Bool | |
eval : ∀ {t : type} → exp t → fromType t | |
eval (nat n) = n | |
eval (plus n m) = eval n + eval m | |
eval (bool b) = b | |
eval (and a b) = eval a ∧ eval b | |
opt : ∀ {t : type} → exp t → exp t | |
opt (nat n) = nat n | |
opt (plus n m) with opt n | opt m | |
... | nat 0 | y = y | |
... | x | nat 0 = x | |
... | x | y = plus x y | |
opt (bool b) = bool b | |
opt (and a b) with opt a | opt b | |
... | bool true | y = y | |
... | x | bool true = x | |
... | x | y = and x y |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Thanks to @pigworker. I had to introduce a datatype to encode the types that LittleLang operates on and index
exp
by that.