GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → jespercockx → ataca

jespercockx / ataca

Licence: other
A TACtic library for Agda

Programming Languages

Agda
84 projects

Labels

tacticsagdaproof-search

Projects that are alternatives of or similar to ataca

MtacAR
Mtac in Agda
Stars: ✭ 29 (-38.3%)
Mutual labels:  tactics, agda
gentle-intro-to-reflection
A slow-paced introduction to reflection in Agda. ---Tactics!
Stars: ✭ 58 (+23.4%)
Mutual labels:  tactics, agda
gapt
GAPT: General Architecture for Proof Theory
Stars: ✭ 83 (+76.6%)
Mutual labels:  tactics
frp agda
Functional Reactive Programming with Agda
Stars: ✭ 22 (-53.19%)
Mutual labels:  agda
CoqCheatSheet
Reference sheet for the Coq language.
Stars: ✭ 15 (-68.09%)
Mutual labels:  tactics
r6maps
Rainbow Six Siege map quick references
Stars: ✭ 74 (+57.45%)
Mutual labels:  tactics
agda-fragment
Algebraic proof discovery in Agda
Stars: ✭ 28 (-40.43%)
Mutual labels:  agda
agda-from-nothing
A workshop on learning Agda with minimal prerequisites.
Stars: ✭ 74 (+57.45%)
Mutual labels:  agda
agda-mode
Accessing Agda's interaction mode via command line & external tactic for Agda.
Stars: ✭ 26 (-44.68%)
Mutual labels:  agda
pgn-tactics-generator
Generate chess puzzles / tactics from a pgn file
Stars: ✭ 83 (+76.6%)
Mutual labels:  tactics
universe-of-syntax
A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.
Stars: ✭ 16 (-65.96%)
Mutual labels:  agda
language-agda
Agda language support for the Atom editor
Stars: ✭ 13 (-72.34%)
Mutual labels:  agda
LibHyps
A Coq library providing tactics to deal with hypothesis
Stars: ✭ 14 (-70.21%)
Mutual labels:  tactics
cubical-categories
Category theory formalized in cubical agda
Stars: ✭ 20 (-57.45%)
Mutual labels:  agda
rekenaar
Idris tactics for (commutative) monoids
Stars: ✭ 21 (-55.32%)
Mutual labels:  tactics
TypeTopology
Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.
Stars: ✭ 132 (+180.85%)
Mutual labels:  agda
Agda
Agda is a dependently typed programming language / interactive theorem prover.
Stars: ✭ 1,699 (+3514.89%)
Mutual labels:  agda
agda-language-server
Language Server for Agda
Stars: ✭ 81 (+72.34%)
Mutual labels:  agda
TacticTurnBased
Prototipo inicial de un juego tactico. Este proyecto solo alberga unos pocos assets con licencia free y el core de un sistema de combate tactico por turnos.
Stars: ✭ 28 (-40.43%)
Mutual labels:  tactics
cat
A formalization of category theory in cubical Agda
Stars: ✭ 50 (+6.38%)
Mutual labels:  agda
View All Similar Projects ➔

ataca: A TACtic library for Agda

This library provides an interface for writing tactics for Agda. It also provides several basic tactics and tactic combinators.

Currently the following tactics are supported:

  • exact: solve a goal with an explicitly given value
  • admit: solve a goal by creating a new postulate
  • assumption: search the context for a variable that fits the goal
  • intro: refine the goal by introducing a lambda
  • intros: refine the goal by introducing as many lambdas as possible
  • introAbsurd: solve the goal with an absurd lambda
  • introConstructor: refine the goal by introducing a constructor that fits the hole
  • introConstructors: refine the goal by repeatedly introducing constructors that fit the (sub)goals
  • refine: refine the goal with a given term applied to some arguments
  • mini-auto: repeatedly apply assumption, intro, and introConstructor
  • mini-auto-with: repeatedly apply assumption, intro, introConstructor, and refine with terms from a given list of hints
  • destruct: case split on the given variable (using a pattern-matching lambda)

The library is currently still work in progress and anything is subject to change at any time.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].