open import Data.Char
open import Data.List as List
open import Function
import Data.String as String
data Token : Set where
a′ b′ c′ x′ +′ : Token
s : String.String → List Token
s = List.map (λ { 'a' → a′ ; 'b' → b′ ; 'c' → c′ ; 'x' → x′ ; '+' → +′ }) ∘ String.toList
Checking this program yields:
Checking T (/private/tmp/T.agda).
/private/tmp/T.agda:10,19-22
Panic: de Bruijn index out of scope: 0 in context []
when checking that the pattern 'a' has type _A_16
I'm using Agda version 2.6.4.3
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4