Skip to content

Instantly share code, notes, and snippets.

@ice1000

ice1000/Andrej.agda

Last active December 14, 2022 20:59
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 ice1000/78405bbf65c7a16f33731414dd3703e5 to your computer and use it in GitHub Desktop.
Save ice1000/78405bbf65c7a16f33731414dd3703e5 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Andrej.agda
{-# OPTIONS --cubical #-}
open import Cubical.Data.Nat.Base hiding (_∸_)
open import Cubical.Core.Everything
data Andrej : Set where
Tesla Zhang : ℕ -> Andrej
Bauer : Tesla 7 ≡ Zhang 6
demo : Andrej -> ℕ
demo (Tesla 0) = 0
demo (Tesla 1) = 0
demo (Tesla (suc x)) = suc (demo (Tesla x))
demo (Zhang 0) = 0
demo (Zhang (suc x)) = suc (demo (Zhang x))
demo (Bauer i) = 6
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment