kmx.io/prism.js/tests/languages/agda/data_feature.test

Branch - branch -master

• Show log

  Commit

• Hash : e644178b
  Author :
  Date : 2020-12-28T18:19:11
  

  Added test for polynomial backtracking (#2597)

Download

• tests/languages/agda/data_feature.test

• data _≐_ {ℓ} {A : Set ℓ} (x : A) : A → Prop ℓ where
  	refl : x ≐ x
  
  ----------------------------------------------------
  
  [
  	["keyword", "data"],
  	["class-name", "_≐_"],
  	["punctuation", "{"],
  	"ℓ",
  	["punctuation", "}"],
  	["punctuation", "{"],
  	["function", "A "],
  	["operator", ":"],
  	["keyword", "Set"],
  	" ℓ",
  	["punctuation", "}"],
  	["punctuation", "("],
  	["function", "x "],
  	["operator", ":"],
  	" A",
  	["punctuation", ")"],
  	["operator", ":"],
  	" A ",
  	["operator", "→"],
  	" Prop ℓ ",
  	["keyword", "where"],
  	["function", "refl "],
  	["operator", ":"],
  	" x ≐ x"
  ]
  
  ----------------------------------------------------
  
  The `data` keyword in Agda is used to declare a type (of course it can be dependent)
  in a fashion like Haskell's GADTs.
  

Download