rodrigogribeiro

Implementação de fatorial usando a linguagem C

Introdução

O objetivo destas notas é apresentar aos alunos o org-mode, um componente do GNU-Emacs que provê suporte a literate programming, isto é, desenvolvimento de programas e sua respectiva documentação em um único formato de arquivo.

rodrigogribeiro

{- Here is a short demonstration on how to use Agda's solvers that automatically
   prove equations. It seems quite impossible to find complete worked examples
   of how Agda solvers are used.

   Thanks go to @anormalform who helped out with these on Twitter, see
   https://twitter.com/andrejbauer/status/1549693506922364929?s=20&t=7cb1TbB2cspIgktKXU8rng

   I welcome improvements and additions to this file.

   This file works with Agda 2.6.2.2 and standard-library-1.7.1

rodrigogribeiro

module Data.Nat.Div.DivIntrinsic where

open import Basics.Admit

open import Data.Nat.Nat
open import Data.Nat.NatTheorems
open import Data.Product.Product
open import Data.Sigma.Sigma
open import Relation.Induction.Natural
open import Relation.Induction.WellFounded

rodrigogribeiro

open import Data.Empty   using (⊥ ; ⊥-elim)
open import Data.List    using (List ; _∷_ ; [] ; length ; _++_)
open import Data.Nat     using (ℕ ; zero ; suc ; _<?_)
open import Data.Product using (_×_ ; proj₁ ; proj₂ ; _,_)
open import Data.Sum     using (_⊎_ ; inj₁ ; inj₂ ; [_,_])

open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Relation.Nullary
open import Relation.Unary

rodrigogribeiro

open import Data.Nat hiding (_⊔_ ; _⊓_)
open import Data.Bool
open import Data.Empty
open import Data.List renaming (_∷_ to _::_) hiding (drop)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any hiding (map)
open import Data.List.Relation.Unary.All renaming (lookup to Alookup) hiding (map)
open import Data.Maybe hiding (map)
open import Data.Product hiding (map)
open import Data.Sum hiding (map)

rodrigogribeiro

#lang brag

i-program : (i-statement)*

; statements syntax

@i-statement : i-assign | i-if | i-skip | i-while | i-print
i-assign     : i-id /"=" i-exp /";"
@i-block     : /"{" (i-statement)* /"}"
i-condition  : /"(" i-exp /")" 

rodrigogribeiro

open import Data.Bool
open import Data.Nat
open import Data.List renaming (_∷_ to _::_)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All renaming (lookup to Alookup)
open import Data.Maybe
open import Data.Product
open import Data.Unit

rodrigogribeiro

\documentclass[9pt]{entcs} 

\usepackage{entcsmacro}
\usepackage{graphicx}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsfonts}
\usepackage{proof}
\usepackage{mathtools}

rodrigogribeiro

module Teste where


next :: Int -> Int
next n
  | even n = n `div` 2
  | otherwise = 3 * n + 1


steps :: Int -> Int

rodrigogribeiro

module Teste where


next :: Int -> Int
next n
  | even n = n `div` 2
  | otherwise = 3 * n + 1


steps :: Int -> Int