Max S. New maxsnew

maxsnew / GuardedKanren.agda

Last active September 4, 2024 14:51 — forked from rntz/GuardedKanren.agda

implementation of muKanren's search strategy in Agda with --guarded

	{-# OPTIONS --guarded #-}
	module GuardedKanren where

	open import Agda.Primitive using (Level; _⊔_)
	private variable
	l l' : Level
	A B : Set l

	data Bool : Set where true false : Bool
	if_then_else_ : ∀{A : Set} → Bool → A → A → A