ziman

# Maintainer: Meow < leon.tty1 at gmail dot com >

# NOTE: If you are experiencing segmentation fault, delete the ".rstudio-desktop" folder from your home directory then restart the program should fix the issue.

pkgname=rstudio-desktop-bin
pkgver=1.4.1717
pkgrel=1
pkgdesc="An integrated development environment (IDE) for R (binary from RStudio official repository)"
arch=('x86_64')
license=('GPL')

ziman

data T : Nat -> Type where
    C : .(n : Nat) -> T n

f : (n : Nat) -> T n -> Bool
f    Z  (C    Z ) = True
f (S n) (C (S n)) = f n (C n)

main : IO ()
main = print $ f 3 (C 3)

ziman

module er where

------------------------

data Erased (A : Set) : Set where
  E : A -> Erased A

pure : {A : Set} -> A -> Erased A
pure = E
  

ziman

module Er

%default total

{- module Erasure; inlined for convenience -}

data Erased : Type -> Type where
  E : a -> Erased a

instance Functor Erased where