De Bruijn indices

Run Settings
LanguageIdris
Language Version
Run Command
module Main import Data.Fin data Term : Nat -> Type where BVar : Fin n -> Term n FVar : String -> Term n Abs : Term (n + 1) -> Term n App : Term n -> Term n -> Term n exampleId : Term 0 exampleId = Abs (BVar 0) exampleConst : Term 0 exampleConst = Abs (Abs (BVar 1)) -- exampleIll : Term 0 -- exampleIll = BVar 0 main : IO () main = putStrLn "Hello World!"
Editor Settings
Theme
Key bindings
Full width
Lines