Skip to content

Instantly share code, notes, and snippets.

@karroffel

karroffel/idris2_multiplicities.idr

Created May 26, 2020 19:09
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save karroffel/a78e9babaadba83aac62849ebd669c44 to your computer and use it in GitHub Desktop.
Save karroffel/a78e9babaadba83aac62849ebd669c44 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
idris2_multiplicities.idr
plus' : (1 a : Nat) -> (1 b : Nat) -> Nat
plus' 0 b = b
plus' (S k) b = S (plus' k b)
data NatE = ZE | SE NatE
plusE : (1 a : NatE) -> (1 b : NatE) -> NatE
plusE ZE b = b
plusE (SE x) b = SE (plusE x b)
data NatG : Type where
ZG : NatG
SG : NatG -> NatG
plusG : (1 a : NatG) -> (1 b : NatG) -> NatG
plusG ZG b = b
plusG (SG x) b =
-- SG (plusG x b) -- doesn't work
?todo
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment