Skip to content

Instantly share code, notes, and snippets.

@msmorgan

msmorgan/Triv.idr

Created October 5, 2017 03:24
Show Gist options
  • Save msmorgan/e0527486244af11de2e1f49b08f41799 to your computer and use it in GitHub Desktop.
Save msmorgan/e0527486244af11de2e1f49b08f41799 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Triv.idr
module Triv
import Data.Vect
%default total
triv : {x : a} -> a
triv {x} = x
oneTwoThree : (n ** Vect n Nat)
oneTwoThree = (triv ** [1, 2, 3])
-- works the same as using (_ ** [1, 2, 3])
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment