Differential D27797 Diff 77175 autotests/folding/test.agda.fold

Changeset View

Standalone View

autotests/folding/test.agda.fold

This file was added.

		1		<indentfold>-- Agda Sample File
		2		-- https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda
		3
		4		-- This test file currently lacks module-related stuff.
		5
		6		</indentfold><beginfold id='1'>{-</beginfold id='1'> Nested
		7		<indentfold> <beginfold id='1'>{-</beginfold id='1'> comment. <endfold id='1'>-}</endfold id='1'> <endfold id='1'>-}</endfold id='1'>
		8
		9		module Test where
		10
		11		infix 12 _!
		12		infixl 7 _+_ _-_
		13		infixr 2 -_
		14
		15		postulate x : Set
		16
		17		f : (Set -> Set -> Set) -> Set
		18		f __ = x x
		19
		20		data ℕ : Set where
		21		zero : ℕ
		22		suc : ℕ -> ℕ
		23
		24		_+_ : ℕ -> ℕ -> ℕ
		25		zero + n = n
		26		suc m + n = suc (m + n)
		27
		28		postulate _-_ : ℕ -> ℕ -> ℕ
		29
		30		-_ : ℕ -> ℕ
		31		- n = n
		32
		33		_! : ℕ -> ℕ
		34		zero ! = suc zero
		35		suc n ! = n - n !
		36
		37		record Equiv {a : Set} (_≈_ : a -> a -> Set) : Set where
		38		field
		39		refl : forall x -> x ≈ x
		40		sym : {x y : a} -> x ≈ y -> y ≈ x
		41		_`trans`_ : forall {x y z} -> x ≈ y -> y ≈ z -> x ≈ z
		42
		43		data _≡_ {a : Set} (x : a) : a -> Set where
		44		refl : x ≡ x
		45
		46		subst : forall {a x y} ->
		47		(P : a -> Set) -> x ≡ y -> P x -> P y
		48		subst {x = x} .{y = x} _ refl p = p
		49
		50		Equiv-≡ : forall {a} -> Equiv {a} _≡_
		51		Equiv-≡ {a} =
		52		record { refl = \_ -> refl
		53		; sym = sym
		54		; _`trans`_ = _`trans`_
		55		}
		56		where
		57		sym : {x y : a} -> x ≡ y -> y ≡ x
		58		sym refl = refl
		59
		60		_`trans`_ : {x y z : a} -> x ≡ y -> y ≡ z -> x ≡ z
		61		refl `trans` refl = refl
		62
		63		postulate
		64		String : Set
		65		Char : Set
		66		Float : Set
		67
		68		data Int : Set where
		69		pos : ℕ → Int
		70		negsuc : ℕ → Int
		71
		72		{-# BUILTIN STRING String #-}
		73		{-# BUILTIN CHAR Char #-}
		74		{-# BUILTIN FLOAT Float #-}
		75
		76		{-# BUILTIN NATURAL ℕ #-}
		77
		78		{-# BUILTIN INTEGER Int #-}
		79		{-# BUILTIN INTEGERPOS pos #-}
		80		{-# BUILTIN INTEGERNEGSUC negsuc #-}
		81
		82		data [_] (a : Set) : Set where
		83		[] : [ a ]
		84		_∷_ : a -> [ a ] -> [ a ]
		85
		86		{-# BUILTIN LIST [_] #-}
		87		{-# BUILTIN NIL [] #-}
		88		{-# BUILTIN CONS _∷_ #-}
		89
		90		primitive
		91		primStringToList : String -> [ Char ]
		92
		93		string : [ Char ]
		94		string = primStringToList "∃ apa"
		95
		96		char : Char
		97		char = '∀'
		98
		99		anotherString : String
		100		anotherString = "¬ be\
		101		\pa"
		102
		103		nat : ℕ
		104		nat = 45
		105
		106		float : Float
		107		float = 45.0e-37
		108
		109		-- Testing qualified names.
		110
		111		open import Test
		112		Eq = Test.Equiv {Test.ℕ}