Luna lunalunaa

jespercockx / ElaboratorReflection.agda

Created January 22, 2022 17:15

	open import Data.Bool.Base
	open import Data.List.Base
	open import Data.Nat.Base
	open import Data.Product
	open import Data.Unit

	open import Function

	open import Reflection
	open import Reflection.TypeChecking.Monad.Syntax

jespercockx / AnyMacro.agda

Created November 5, 2021 16:44

	--{-# OPTIONS -v any-auto:10 #-}

	open import Data.List
	open import Data.List.Membership.Propositional using (_∈_)
	open import Data.List.Relation.Unary.Any using (Any; here; there)
	open import Data.List.Relation.Unary.Any.Properties using
	(singleton⁺; map⁺; mapMaybe⁺; ++⁺ˡ; ++⁺ʳ; concat⁺)
	open import Data.Maybe using (Maybe; nothing; just)
	open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
	open import Data.Nat using (ℕ; zero; suc; _+_)

y-taka-23 / coq_filter.v

Last active May 21, 2018 03:26

Validation of the filter Function (via "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/Logic.html)

	(******************************************************)
	(** //// Validation of the "filter" Function //// *)
	(******************************************************)

	Require Import List Bool Lt.

	Section Filter.


	(////////////////////////////////////////////////////)